From 5548891f2cd9a50e33e889c4ca95518ecc8bf4dc Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Mon, 1 Sep 2025 16:24:53 +0200
Subject: [PATCH 1/3] add equality theorems

---
 discouraged |  10 +
 set.mm      | 778 ++++++++++++++++++++++++++++++++++++++++++++++++----
 2 files changed, 737 insertions(+), 51 deletions(-)

diff --git a/discouraged b/discouraged
index 8ef2f9c9cb..0088e80418 100644
--- a/discouraged
+++ b/discouraged
@@ -17673,9 +17673,11 @@ New usage of "isvciOLD" is discouraged (3 uses).
 New usage of "isvclem" is discouraged (1 uses).
 New usage of "iswatN" is discouraged (0 uses).
 New usage of "itg1addlem4OLD" is discouraged (0 uses).
+New usage of "itgeq1fOLD" is discouraged (0 uses).
 New usage of "itvndx" is discouraged (6 uses).
 New usage of "iunconnALT" is discouraged (0 uses).
 New usage of "iunconnlem2" is discouraged (1 uses).
+New usage of "iuneq12dOLD" is discouraged (0 uses).
 New usage of "iunidOLD" is discouraged (0 uses).
 New usage of "iunopabOLD" is discouraged (0 uses).
 New usage of "ivthALT" is discouraged (0 uses).
@@ -18898,6 +18900,8 @@ New usage of "prn0" is discouraged (8 uses).
 New usage of "prnmadd" is discouraged (2 uses).
 New usage of "prnmax" is discouraged (7 uses).
 New usage of "probfinmeasbALTV" is discouraged (0 uses).
+New usage of "prodeq1iOLD" is discouraged (0 uses).
+New usage of "prodeq2sdvOLD" is discouraged (0 uses).
 New usage of "prpssnq" is discouraged (8 uses).
 New usage of "prstchom2ALT" is discouraged (0 uses).
 New usage of "prstchomval" is discouraged (3 uses).
@@ -18951,6 +18955,7 @@ New usage of "r1pid2OLD" is discouraged (0 uses).
 New usage of "r1pwALT" is discouraged (0 uses).
 New usage of "rabbidaOLD" is discouraged (0 uses).
 New usage of "rabbiiaOLD" is discouraged (0 uses).
+New usage of "rabeqbidvaOLD" is discouraged (0 uses).
 New usage of "rabeqcOLD" is discouraged (0 uses).
 New usage of "rabexgOLD" is discouraged (0 uses).
 New usage of "rabid2OLD" is discouraged (0 uses).
@@ -21143,8 +21148,10 @@ Proof modification of "istrkg2d" is discouraged (439 steps).
 Proof modification of "isvcOLD" is discouraged (170 steps).
 Proof modification of "isvciOLD" is discouraged (178 steps).
 Proof modification of "itg1addlem4OLD" is discouraged (1803 steps).
+Proof modification of "itgeq1fOLD" is discouraged (152 steps).
 Proof modification of "iunconnALT" is discouraged (56 steps).
 Proof modification of "iunconnlem2" is discouraged (580 steps).
+Proof modification of "iuneq12dOLD" is discouraged (37 steps).
 Proof modification of "iunidOLD" is discouraged (77 steps).
 Proof modification of "iunopabOLD" is discouraged (117 steps).
 Proof modification of "ivthALT" is discouraged (1080 steps).
@@ -21431,6 +21438,8 @@ Proof modification of "problem2" is discouraged (104 steps).
 Proof modification of "problem3" is discouraged (56 steps).
 Proof modification of "problem4" is discouraged (310 steps).
 Proof modification of "problem5" is discouraged (133 steps).
+Proof modification of "prodeq1iOLD" is discouraged (19 steps).
+Proof modification of "prodeq2sdvOLD" is discouraged (16 steps).
 Proof modification of "prstchom2ALT" is discouraged (121 steps).
 Proof modification of "prstclevalOLD" is discouraged (86 steps).
 Proof modification of "prstcocvalOLD" is discouraged (88 steps).
@@ -21459,6 +21468,7 @@ Proof modification of "r1pid2OLD" is discouraged (496 steps).
 Proof modification of "r1pwALT" is discouraged (151 steps).
 Proof modification of "rabbidaOLD" is discouraged (36 steps).
 Proof modification of "rabbiiaOLD" is discouraged (39 steps).
+Proof modification of "rabeqbidvaOLD" is discouraged (28 steps).
 Proof modification of "rabeqcOLD" is discouraged (37 steps).
 Proof modification of "rabexgOLD" is discouraged (21 steps).
 Proof modification of "rabid2OLD" is discouraged (57 steps).
diff --git a/set.mm b/set.mm
index 5ad01a1bd1..d8ed1ac996 100644
--- a/set.mm
+++ b/set.mm
@@ -31490,14 +31490,14 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
 
   ${
     rmobiia.1 $e |- ( x e. A -> ( ph <-> ps ) ) $.
-    $( Formula-building rule for restricted existential quantifier (inference
+    $( Formula-building rule for restricted at-most-one quantifier (inference
        form).  (Contributed by NM, 16-Jun-2017.) $)
     rmobiia $p |- ( E* x e. A ph <-> E* x e. A ps ) $=
       ( cv wcel wa wmo wrmo pm5.32i mobii df-rmo 3bitr4i ) CFDGZAHZCIOBHZCIACDJ
       BCDJPQCOABEKLACDMBCDMN $.
 
-    $( Formula-building rule for restricted existential quantifier (inference
-       form).  (Contributed by NM, 14-Nov-2004.) $)
+    $( Formula-building rule for restricted existential uniqueness quantifier
+       (inference form).  (Contributed by NM, 14-Nov-2004.) $)
     reubiia $p |- ( E! x e. A ph <-> E! x e. A ps ) $=
       ( cv wcel wa weu wreu pm5.32i eubii df-reu 3bitr4i ) CFDGZAHZCIOBHZCIACDJ
       BCDJPQCOABEKLACDMBCDMN $.
@@ -31505,13 +31505,13 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
 
   ${
     rmobii.1 $e |- ( ph <-> ps ) $.
-    $( Formula-building rule for restricted existential quantifier (inference
+    $( Formula-building rule for restricted at-most-one quantifier (inference
        form).  (Contributed by NM, 16-Jun-2017.) $)
     rmobii $p |- ( E* x e. A ph <-> E* x e. A ps ) $=
       ( wb cv wcel a1i rmobiia ) ABCDABFCGDHEIJ $.
 
-    $( Formula-building rule for restricted existential quantifier (inference
-       form).  (Contributed by NM, 22-Oct-1999.) $)
+    $( Formula-building rule for restricted existential uniqueness quantifier
+       (inference form).  (Contributed by NM, 22-Oct-1999.) $)
     reubii $p |- ( E! x e. A ph <-> E! x e. A ps ) $=
       ( wb cv wcel a1i reubiia ) ABCDABFCGDHEIJ $.
   $}
@@ -31552,7 +31552,7 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
   ${
     $d x ph $.
     rmobidva.1 $e |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) ) $.
-    $( Formula-building rule for restricted existential quantifier (deduction
+    $( Formula-building rule for restricted at-most-one quantifier (deduction
        form).  (Contributed by NM, 16-Jun-2017.)  Avoid ~ ax-6 , ~ ax-7 ,
        ~ ax-12 .  (Revised by Wolf Lammen, 23-Nov-2024.) $)
     rmobidva $p |- ( ph -> ( E* x e. A ps <-> E* x e. A ch ) ) $=
@@ -31560,9 +31560,9 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
       DEKCDEKAQRDAPBCFLMBDENCDENO $.
     $( $j usage 'rmobidva' avoids 'ax-6' 'ax-7' 'ax-12'; $)
 
-    $( Formula-building rule for restricted existential quantifier (deduction
-       form).  (Contributed by NM, 13-Nov-2004.)  Reduce axiom usage.  (Revised
-       by Wolf Lammen, 14-Jan-2023.) $)
+    $( Formula-building rule for restricted existential uniqueness quantifier
+       (deduction form).  (Contributed by NM, 13-Nov-2004.)  Reduce axiom
+       usage.  (Revised by Wolf Lammen, 14-Jan-2023.) $)
     reubidva $p |- ( ph -> ( E! x e. A ps <-> E! x e. A ch ) ) $=
       ( cv wcel wa weu wreu pm5.32da eubidv df-reu 3bitr4g ) ADGEHZBIZDJPCIZDJB
       DEKCDEKAQRDAPBCFLMBDENCDENO $.
@@ -31571,13 +31571,13 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
   ${
     $d x ph $.
     rmobidv.1 $e |- ( ph -> ( ps <-> ch ) ) $.
-    $( Formula-building rule for restricted existential quantifier (deduction
+    $( Formula-building rule for restricted at-most-one quantifier (deduction
        form).  (Contributed by NM, 16-Jun-2017.) $)
     rmobidv $p |- ( ph -> ( E* x e. A ps <-> E* x e. A ch ) ) $=
       ( wb cv wcel adantr rmobidva ) ABCDEABCGDHEIFJK $.
 
-    $( Formula-building rule for restricted existential quantifier (deduction
-       form).  (Contributed by NM, 17-Oct-1996.) $)
+    $( Formula-building rule for restricted existential uniqueness quantifier
+       (deduction form).  (Contributed by NM, 17-Oct-1996.) $)
     reubidv $p |- ( ph -> ( E! x e. A ps <-> E! x e. A ch ) ) $=
       ( wb cv wcel adantr reubidva ) ABCDEABCGDHEIFJK $.
   $}
@@ -32133,17 +32133,31 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
   $}
 
   ${
-    $d A x $.  $d B x $.  $d ph x $.
+    $d ph x $.
     rabeqbidva.1 $e |- ( ph -> A = B ) $.
     rabeqbidva.2 $e |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) ) $.
     $( Equality of restricted class abstractions.  (Contributed by Mario
-       Carneiro, 26-Jan-2017.) $)
+       Carneiro, 26-Jan-2017.)  Remove DV conditions.  (Revised by GG,
+       1-Sep-2025.) $)
     rabeqbidva $p |- ( ph -> { x e. A | ps } = { x e. B | ch } ) $=
-      ( crab rabbidva rabeqdv eqtrd ) ABDEICDEICDFIABCDEHJACDEFGKL $.
+      ( crab rabbidva cv wcel eleq2d anbi1d rabbidva2 eqtrd ) ABDEICDEICDFIABCD
+      EHJACCDEFADKZELQFLCAEFQGMNOP $.
+    $( $j usage 'rabeqbidva' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
   $}
 
   ${
     $d A x $.  $d B x $.  $d ph x $.
+    rabeqbidvaOLD.1 $e |- ( ph -> A = B ) $.
+    rabeqbidvaOLD.2 $e |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) ) $.
+    $( Obsolete version of ~ rabeqbidva as of 1-Sep-2025.  (Contributed by
+       Mario Carneiro, 26-Jan-2017.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    rabeqbidvaOLD $p |- ( ph -> { x e. A | ps } = { x e. B | ch } ) $=
+      ( crab rabbidva rabeqdv eqtrd ) ABDEICDEICDFIABCDEHJACDEFGKL $.
+  $}
+
+  ${
+    $d ph x $.
     rabeqbidv.1 $e |- ( ph -> A = B ) $.
     rabeqbidv.2 $e |- ( ph -> ( ps <-> ch ) ) $.
     $( Equality of restricted class abstractions.  (Contributed by Jeff Madsen,
@@ -47563,11 +47577,13 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
        3-Aug-2004.) $)
     iuneq2dv $p |- ( ph -> U_ x e. A B = U_ x e. A C ) $=
       ( wceq wral ciun ralrimiva iuneq2 syl ) ADEGZBCHBCDIBCEIGAMBCFJBCDEKL $.
+    $( $j usage 'iuneq2dv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
 
     $( Equality deduction for indexed intersection.  (Contributed by NM,
        3-Aug-2004.) $)
     iineq2dv $p |- ( ph -> |^|_ x e. A B = |^|_ x e. A C ) $=
-      ( nfv iineq2d ) ABCDEABGFH $.
+      ( wceq wral ciin ralrimiva iineq2 syl ) ADEGZBCHBCDIBCEIGAMBCFJBCDEKL $.
+    $( $j usage 'iineq2dv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
   $}
 
   ${
@@ -47595,15 +47611,30 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
 
     ${
       $d x ph $.
-      iuneq12d.2 $e |- ( ph -> C = D ) $.
-      $( Equality deduction for indexed union, deduction version.  (Contributed
-         by Drahflow, 22-Oct-2015.) $)
-      iuneq12d $p |- ( ph -> U_ x e. A C = U_ x e. B D ) $=
+      iuneq12dOLD.2 $e |- ( ph -> C = D ) $.
+      $( Obsolete version of ~ iuneq12d as of 1-Sep-2025.  (Contributed by
+         Drahflow, 22-Oct-2015.)  (Proof modification is discouraged.)
+         (New usage is discouraged.) $)
+      iuneq12dOLD $p |- ( ph -> U_ x e. A C = U_ x e. B D ) $=
         ( ciun iuneq1d wceq cv wcel adantr iuneq2dv eqtrd ) ABCEIBDEIBDFIABCDEG
         JABDEFAEFKBLDMHNOP $.
     $}
   $}
 
+  ${
+    $d x t ph $.  $d A t $.  $d B t $.  $d C t $.
+    iuneq12d.1 $e |- ( ph -> A = B ) $.
+    iuneq12d.2 $e |- ( ph -> C = D ) $.
+    $( Equality deduction for indexed union, deduction version.  (Contributed
+       by Drahflow, 22-Oct-2015.)  Remove DV conditions (Revised by GG,
+       1-Sep-2025.) $)
+    iuneq12d $p |- ( ph -> U_ x e. A C = U_ x e. B D ) $=
+      ( vt ciun cv wcel wrex cab eleq2d anbi1d rexbidv2 abbidv df-iun 3eqtr4g
+      wceq adantr iuneq2dv eqtrd ) ABCEJZBDEJZBDFJAIKELZBCMZINUGBDMZINUEUFAUHUI
+      IAUGUGBCDABKZCLUJDLZUGACDUJGOPQRBICESBIDESTABDEFAEFUAUKHUBUCUD $.
+    $( $j usage 'iuneq12d' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
   ${
     $d x ph $.
     iuneq2d.2 $e |- ( ph -> B = C ) $.
@@ -177673,7 +177704,6 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/
   $}
 
   ${
-    $d k A $.  $d k B $.
     sumeq1i.1 $e |- A = B $.
     $( Equality inference for sum.  (Contributed by NM, 2-Jan-2006.) $)
     sumeq1i $p |- sum_ k e. A C = sum_ k e. B C $=
@@ -177698,7 +177728,6 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/
   $}
 
   ${
-    $d k A $.  $d k B $.
     sumeq1d.1 $e |- ( ph -> A = B ) $.
     $( Equality deduction for sum.  (Contributed by NM, 1-Nov-2005.) $)
     sumeq1d $p |- ( ph -> sum_ k e. A C = sum_ k e. B C ) $=
@@ -177724,7 +177753,7 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/
   $}
 
   ${
-    $d k x m n f A $.  $d x m n f B $.  $d x m n f C $.  $d k x m n f ph $.
+    $d x m n f A $.  $d x m n f B $.  $d x m n f C $.  $d k x m n f ph $.
     sumeq2sdv.1 $e |- ( ph -> B = C ) $.
     $( Equality deduction for sum.  (Contributed by NM, 3-Jan-2006.)  (Proof
        shortened by Glauco Siliprandi, 5-Apr-2020.)  Avoid axioms.  (Revised by
@@ -177739,7 +177768,8 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/
       AWMXIAWAWTGNAVTWSVLAVRWRVSUGAVQWQMVKAHNVPWPAVNVOWOUCAEVMCDFUPUQURUSVAVBVC
       AWLXHGTAWKXGJAWJXFWDAWIXEVSAVKWHXDAWGXCMUEAHTWFXBAEWECDFUPURUSVDVEVBVFVCV
       GVHIBCJEGHVJIBDJEGHVJVI $.
-    $( $j usage 'sumeq2sdv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+    $( $j usage 'sumeq2sdv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13' 'ax-sep'
+       'ax-nul' 'ax-pow' 'ax-pr' 'ax-un'; $)
   $}
 
   ${
@@ -182894,11 +182924,21 @@ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/
   $}
 
   ${
-    $d A k $.  $d B k $.
+    $d A k x y m n f $.  $d B k x y m n f $.  $d C x y m n f $.
     $( Equality theorem for a product.  (Contributed by Scott Fenton,
        1-Dec-2017.) $)
     prodeq1 $p |- ( A = B -> prod_ k e. A C = prod_ k e. B C ) $=
-      ( nfcv prodeq1f ) ABCDDAEDBEF $.
+      ( vm vy vn vx vf cv cmul cz c1 cseq cli wbr wa wex wrex cn wceq wcel cmpt
+      cuz cfv wss cc0 wne cif w3a cfz co wf1o csb wo cprod sseq1 eleq2 mpteq2dv
+      cio seqeq3d breq1d anbi2d exbidv rexbidv 3anbi123d f1oeq3 anbi1d iotabidv
+      ifbid orbi12d df-prod 3eqtr4g ) ABUAZAEJZUDUEZUFZFJZUGUHZKDLDJZAUBZCMUIZU
+      CZGJZNZVROPZQZFRZGVPSZKWCVONZHJZOPZUJZELSZMVOUKULZAIJZUMZWKVOKGTDWDWPUECU
+      NUCMNUEUAZQZIRZETSZUOZHUTBVPUFZVSKDLVTBUBZCMUIZUCZWDNZVROPZQZFRZGVPSZKXFV
+      ONZWKOPZUJZELSZWOBWPUMZWRQZIRZETSZUOZHUTACDUPBCDUPVNXBXTHVNWNXOXAXSVNWMXN
+      ELVNVQXCWIXKWLXMABVPUQVNWHXJGVPVNWGXIFVNWFXHVSVNWEXGVROVNWCXFKWDVNDLWBXEV
+      NWAXDCMABVTURVJUSZVAVBVCVDVEVNWJXLWKOVNWCXFKVOYAVAVBVFVEVNWTXRETVNWSXQIVN
+      WQXPWRABWOWPVGVHVDVEVKVIHFACIDEGVLHFBCIDEGVLVM $.
+    $( $j usage 'prodeq1' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
   $}
 
   ${
@@ -183060,11 +183100,30 @@ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/
   $}
 
   ${
-    $d k A $.  $d k B $.
+    $d k x y m n f $.  $d A x y m n f $.  $d B x y m n f $.  $d C x y m n f $.
     prodeq1i.1 $e |- A = B $.
     $( Equality inference for product.  (Contributed by Scott Fenton,
-       4-Dec-2017.) $)
+       4-Dec-2017.)  Remove DV conditions.  (Revised by GG, 1-Sep-2025.) $)
     prodeq1i $p |- prod_ k e. A C = prod_ k e. B C $=
+      ( vm vy vn vx vf cv cmul cz c1 cseq cli wbr wa wrex wceq cuz cfv wss wcel
+      cc0 wne cif cmpt wex w3a cfz co wf1o cn csb wo cio cprod sseq1i wb eleq2i
+      ax-mp mpteq2i seqeq3 breq1i anbi2i rexbii 3anbi123i f1oeq3 anbi1i orbi12i
+      ifbi exbii iotabii df-prod 3eqtr4i ) AFKZUAUBZUCZGKZUEUFZLDMDKZAUDZCNUGZU
+      HZHKZOZVTPQZRZGUIZHVRSZLWEVQOZIKZPQZUJZFMSZNVQUKULZAJKZUMZWMVQLHUNDWFWRUB
+      CUOUHNOUBTZRZJUIZFUNSZUPZIUQBVRUCZWALDMWBBUDZCNUGZUHZWFOZVTPQZRZGUIZHVRSZ
+      LXHVQOZWMPQZUJZFMSZWQBWRUMZWTRZJUIZFUNSZUPZIUQACDURBCDURXDYBIWPXQXCYAWOXP
+      FMVSXEWKXMWNXOABVREUSWJXLHVRWIXKGWHXJWAWGXIVTPWEXHTZWGXITDMWDXGWCXFUTWDXG
+      TABWBEVAWCXFCNVLVBVCZLWEXHWFVDVBVEVFVMVGWLXNWMPYCWLXNTYDLWEXHVQVDVBVEVHVG
+      XBXTFUNXAXSJWSXRWTABTWSXRUTEABWQWRVIVBVJVMVGVKVNIGACJDFHVOIGBCJDFHVOVP $.
+  $}
+
+  ${
+    $d k A $.  $d k B $.
+    prodeq1iOLD.1 $e |- A = B $.
+    $( Obsolete version of ~ prodeq1i as of 1-Sep-2025.  (Contributed by Scott
+       Fenton, 4-Dec-2017.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    prodeq1iOLD $p |- prod_ k e. A C = prod_ k e. B C $=
       ( wceq cprod prodeq1 ax-mp ) ABFACDGBCDGFEABCDHI $.
   $}
 
@@ -183115,11 +183174,33 @@ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/
   $}
 
   ${
-    $d k A $.  $d k ph $.
+    $d x y m n f A $.  $d x y m n f B $.  $d x y m n f C $.
+    $d k x y m n f ph $.
     prodeq2sdv.1 $e |- ( ph -> B = C ) $.
     $( Equality deduction for product.  (Contributed by Scott Fenton,
-       4-Dec-2017.) $)
+       4-Dec-2017.)  Avoid axioms.  (Revised by GG, 1-Sep-2025.) $)
     prodeq2sdv $p |- ( ph -> prod_ k e. A B = prod_ k e. A C ) $=
+      ( vm vy vn vx vf cv cfv cmul cz c1 cseq cli wrex cn cuz wss cc0 wcel cmpt
+      wne cif wbr wa wex w3a cfz co wf1o csb wceq wo cio cprod mpteq2dv seqeq3d
+      ifeq1d breq1d anbi2d exbidv rexbidv fveq1d eqeq2d orbi12d df-prod 3eqtr4g
+      3anbi23d csbeq2dv iotabidv ) ABGLZUAMZUBZHLZUCUFZNEOELBUDZCPUGZUEZILZQZVR
+      RUHZUIZHUJZIVPSZNWBVOQZJLZRUHZUKZGOSZPVOULUMBKLZUNZWJVONITEWCWNMZCUOZUEZP
+      QZMZUPZUIZKUJZGTSZUQZJURVQVSNEOVTDPUGZUEZWCQZVRRUHZUIZHUJZIVPSZNXGVOQZWJR
+      UHZUKZGOSZWOWJVONITEWPDUOZUEZPQZMZUPZUIZKUJZGTSZUQZJURBCEUSBDEUSAXEYEJAWM
+      XPXDYDAWLXOGOAWHXLWKXNVQAWGXKIVPAWFXJHAWEXIVSAWDXHVRRAWBXGNWCAEOWAXFAVTCD
+      PFVBUTZVAVCVDVEVFAWIXMWJRAWBXGNVOYFVAVCVLVFAXCYCGTAXBYBKAXAYAWOAWTXTWJAVO
+      WSXSAWRXRNPAITWQXQAEWPCDFVMUTVAVGVHVDVEVFVIVNJHBCKEGIVJJHBDKEGIVJVK $.
+    $( $j usage 'prodeq2sdv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13' 'ax-sep'
+       'ax-nul' 'ax-pow' 'ax-pr' 'ax-un'; $)
+  $}
+
+  ${
+    $d k A $.  $d k ph $.
+    prodeq2sdvOLD.1 $e |- ( ph -> B = C ) $.
+    $( Obsolete version of ~ prodeq2sdv as of 1-Sep-2025.  (Contributed by
+       Scott Fenton, 4-Dec-2017.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    prodeq2sdvOLD $p |- ( ph -> prod_ k e. A B = prod_ k e. A C ) $=
       ( wceq cv wcel adantr prodeq2dv ) ABCDEACDGEHBIFJK $.
   $}
 
@@ -361791,7 +361872,7 @@ or are almost disjoint (the interiors are disjoint).  (Contributed by
   $}
 
   ${
-    $d k x y $.  $d k y A $.  $d k y B $.  $d k C $.
+    $d k x y $.  $d k y A $.  $d k y B $.  $d k y C $.
     $( An integral is a set.  (Contributed by Mario Carneiro, 28-Jun-2014.) $)
     itgex $p |- S. A B _d x e. _V $=
       ( vk vy citg cc0 c3 cfz co ci cv cexp cr cdiv cre cfv wcel cle wbr wa cif
@@ -361801,8 +361882,20 @@ or are almost disjoint (the interiors are disjoint).  (Contributed by
     itgeq1f.1 $e |- F/_ x A $.
     itgeq1f.2 $e |- F/_ x B $.
     $( Equality theorem for an integral.  (Contributed by Mario Carneiro,
-       28-Jun-2014.) $)
+       28-Jun-2014.)  Avoid axioms.  (Revised by GG, 1-Sep-2025.) $)
     itgeq1f $p |- ( A = B -> S. A C _d x = S. B C _d x ) $=
+      ( vk vy wceq cc0 co cv cr cfv wcel wa cif csb citg2 cmul c3 cfz cexp cdiv
+      ci cre cle wbr cmpt citg nfeq eleq2 anbi1d ifbid csbeq2dv adantr mpteq2da
+      csu fveq2d oveq2d sumeq2sdv df-itg 3eqtr4g ) BCIZJUAUBKZUEGLUCKZAMHDVFUDK
+      UFNZALZBOZJHLZUGUHZPZVJJQZRZUIZSNZTKZGURVEVFAMHVGVHCOZVKPZVJJQZRZUIZSNZTK
+      ZGURABDUJACDUJVDVEVQWDGVDVPWCVFTVDVOWBSVDAMVNWAABCEFUKVDVNWAIVHMOVDHVGVMV
+      TVDVLVSVJJVDVIVRVKBCVHULUMUNUOUPUQUSUTVAAHBDGVBAHCDGVBVC $.
+    $( $j usage 'itgeq1f' avoids 'ax-sep' 'ax-nul' 'ax-pow' 'ax-pr' 'ax-un'; $)
+
+    $( Obsolete version of ~ itgeq1f as of 1-Sep-2025.  (Contributed by Mario
+       Carneiro, 28-Jun-2014.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    itgeq1fOLD $p |- ( A = B -> S. A C _d x = S. B C _d x ) $=
       ( vk wceq cc0 co cv cr wcel cfv wa cif cmpt citg2 cmul csu c3 cfz ci cexp
       cdiv cre cle wbr citg wral eqid nfeq eleq2 anbi1d ralrimi mpteq12 sylancr
       ifbid a1d fveq2d oveq2d sumeq2sdv dfitg 3eqtr4g ) BCHZIUAUBJZUCGKUDJZALAK
@@ -361813,11 +361906,18 @@ or are almost disjoint (the interiors are disjoint).  (Contributed by
   $}
 
   ${
-    $d x A $.  $d x B $.
+    $d x y k A $.  $d x y k B $.  $d k y C $.
     $( Equality theorem for an integral.  (Contributed by Mario Carneiro,
        28-Jun-2014.) $)
     itgeq1 $p |- ( A = B -> S. A C _d x = S. B C _d x ) $=
-      ( nfcv itgeq1f ) ABCDABEACEF $.
+      ( vk vy cc0 co cv cr cfv wcel wa cif csb cmpt citg2 cmul csu citg wceq c3
+      cfz ci cexp cdiv cre cle wbr eleq2 anbi1d csbeq2dv mpteq2dv fveq2d oveq2d
+      ifbid sumeq2sdv df-itg 3eqtr4g ) BCUAZGUBUCHZUDEIUEHZAJFDVBUFHUGKZAIZBLZG
+      FIZUHUIZMZVFGNZOZPZQKZRHZESVAVBAJFVCVDCLZVGMZVFGNZOZPZQKZRHZESABDTACDTUTV
+      AVMVTEUTVLVSVBRUTVKVRQUTAJVJVQUTFVCVIVPUTVHVOVFGUTVEVNVGBCVDUJUKUPULUMUNU
+      OUQAFBDEURAFCDEURUS $.
+    $( $j usage 'itgeq1' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13' 'ax-sep'
+       'ax-nul' 'ax-pow' 'ax-pr' 'ax-un'; $)
   $}
 
   ${
@@ -578527,6 +578627,500 @@ conditions of the Five Segment Axiom ( ~ ax5seg ).  See ~ brofs and
 $)
 
 
+$(
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+  Equality theorems.
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+$)
+
+
+$(
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+  Inference versions.
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+$)
+
+  ${
+    rmoeqi.1 $e |- A = B $.
+    $( Equality inference for restricted at-most-one quantifier.  (Contributed
+       by GG, 1-Sep-2025.) $)
+    rmoeqi $p |- ( E* x e. A ps <-> E* x e. B ps ) $=
+      ( cv wcel wa wmo wrmo eleq2i anbi1i mobii df-rmo 3bitr4i ) BFZCGZAHZBIPDG
+      ZAHZBIABCJABDJRTBQSACDPEKLMABCNABDNO $.
+    $( $j usage 'rmoeqi' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    rmoeqbii.1 $e |- A = B $.
+    rmoeqbii.2 $e |- ( ps <-> ch ) $.
+    $( Equality inference for restricted at-most-one quantifier.  (Contributed
+       by GG, 1-Sep-2025.) $)
+    rmoeqbii $p |- ( E* x e. A ps <-> E* x e. B ch ) $=
+      ( cv wcel wa wmo wrmo eleq2i anbi12i mobii df-rmo 3bitr4i ) CHZDIZAJZCKRE
+      IZBJZCKACDLBCELTUBCSUAABDERFMGNOACDPBCEPQ $.
+    $( $j usage 'rmoeqbii' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    reueqi.1 $e |- A = B $.
+    $( Equality inference for restricted existential uniqueness quantifier.
+       (Contributed by GG, 1-Sep-2025.) $)
+    reueqi $p |- ( E! x e. A ps <-> E! x e. B ps ) $=
+      ( cv wcel wa weu wreu eleq2i anbi1i eubii df-reu 3bitr4i ) BFZCGZAHZBIPDG
+      ZAHZBIABCJABDJRTBQSACDPEKLMABCNABDNO $.
+    $( $j usage 'reueqi' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    reueqbii.1 $e |- A = B $.
+    reueqbii.2 $e |- ( ps <-> ch ) $.
+    $( Equality inference for restricted existential uniqueness quantifier.
+       (Contributed by GG, 1-Sep-2025.) $)
+    reueqbii $p |- ( E! x e. A ps <-> E! x e. B ch ) $=
+      ( cv wcel wa weu wreu eleq2i anbi12i eubii df-reu 3bitr4i ) CHZDIZAJZCKRE
+      IZBJZCKACDLBCELTUBCSUAABDERFMGNOACDPBCEPQ $.
+    $( $j usage 'reueqbii' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    sbceqbii.1 $e |- A = B $.
+    sbceqbii.2 $e |- ( ph <-> ps ) $.
+    $( Formula-building inference for class substitution.  General version of
+       ~ sbcbii .  (Contributed by GG, 1-Sep-2025.) $)
+    sbceqbii $p |- ( [. A / x ]. ph <-> [. B / x ]. ps ) $=
+      ( cab wcel wsbc abbii eleq12i df-sbc 3bitr4i ) DACHZIEBCHZIACDJBCEJDEOPFA
+      BCGKLACDMBCEMN $.
+    $( $j usage 'sbceqbii' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d t x $.  $d A t $.  $d B t $.  $d C t $.
+    disjeq1i.1 $e |- A = B $.
+    $( Equality theorem for disjoint collection.  Inference version.
+       (Contributed by GG, 1-Sep-2025.) $)
+    disjeq1i $p |- ( Disj_ x e. A C <-> Disj_ x e. B C ) $=
+      ( vt cv wcel wrmo wal wdisj rmoeqi albii df-disj 3bitr4i ) FGDHZABIZFJPAC
+      IZFJABDKACDKQRFPABCELMAFBDNAFCDNO $.
+    $( $j usage 'disjeq1i' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    disjeq12i.1 $e |- A = B $.
+    disjeq12i.2 $e |- C = D $.
+    $( Equality theorem for disjoint collection.  Inference version.
+       (Contributed by GG, 1-Sep-2025.) $)
+    disjeq12i $p |- ( Disj_ x e. A C <-> Disj_ x e. B D ) $=
+      ( wdisj wceq wb disjeq2 cv wcel a1i mprg disjeq1i bitri ) ABDHZABEHZACEHD
+      EIZRSJABABDEKTALBMGNOABCEFPQ $.
+    $( $j usage 'disjeq12i' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    rabeqbii.1 $e |- A = B $.
+    rabeqbii.2 $e |- ( ph <-> ps ) $.
+    $( Equality theorem for restricted class abstractions.  Inference version.
+       (Contributed by GG, 1-Sep-2025.) $)
+    rabeqbii $p |- { x e. A | ph } = { x e. B | ps } $=
+      ( cv wcel wa cab crab eleq2i anbi12i abbii df-rab 3eqtr4i ) CHZDIZAJZCKRE
+      IZBJZCKACDLBCELTUBCSUAABDERFMGNOACDPBCEPQ $.
+    $( $j usage 'rabeqbii' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d A t $.  $d B t $.  $d C t $.  $d D t $.  $d x t $.
+    iuneq12i.1 $e |- A = B $.
+    iuneq12i.2 $e |- C = D $.
+    $( Equality theorem for indexed union.  Inference version.  (Contributed by
+       GG, 1-Sep-2025.) $)
+    iuneq12i $p |- U_ x e. A C = U_ x e. B D $=
+      ( vt cv wcel wrex cab ciun eleq2i rexeqbii abbii df-iun 3eqtr4i ) HIZDJZA
+      BKZHLSEJZACKZHLABDMACEMUAUCHTUBABCFDESGNOPAHBDQAHCEQR $.
+    $( $j usage 'iuneq12i' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d A t $.  $d B t $.  $d C t $.  $d x t $.
+    iineq1i.1 $e |- A = B $.
+    $( Equality theorem for indexed intersection.  Inference version.
+       (Contributed by GG, 1-Sep-2025.) $)
+    iineq1i $p |- |^|_ x e. A C = |^|_ x e. B C $=
+      ( vt cv wcel wral cab ciin eleq2i imbi1i ralbii2 abbii df-iin 3eqtr4i ) F
+      GDHZABIZFJRACIZFJABDKACDKSTFRRABCAGZBHUACHRBCUAELMNOAFBDPAFCDPQ $.
+    $( $j usage 'iineq1i' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d A t $.  $d B t $.  $d C t $.  $d D t $.  $d x t $.
+    iineq12i.1 $e |- A = B $.
+    iineq12i.2 $e |- C = D $.
+    $( Equality theorem for indexed intersection.  Inference version.  General
+       version of ~ iineq1i .  (Contributed by GG, 1-Sep-2025.) $)
+    iineq12i $p |- |^|_ x e. A C = |^|_ x e. B D $=
+      ( vt cv wcel wral cab ciin eleq2i raleqbii abbii df-iin 3eqtr4i ) HIZDJZA
+      BKZHLSEJZACKZHLABDMACEMUAUCHTUBABCFDESGNOPAHBDQAHCEQR $.
+    $( $j usage 'iineq12i' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    riotaeqbii.1 $e |- A = B $.
+    riotaeqbii.2 $e |- ( ph <-> ps ) $.
+    $( Equivalent wff's and equal domains yield equal restricted iotas.
+       Inference version.  (Contributed by GG, 1-Sep-2025.) $)
+    riotaeqbii $p |- ( iota_ x e. A ph ) = ( iota_ x e. B ps ) $=
+      ( cv wcel wa cio crio eleq2i anbi12i iotabii df-riota 3eqtr4i ) CHZDIZAJZ
+      CKREIZBJZCKACDLBCELTUBCSUAABDERFMGNOACDPBCEPQ $.
+    $( $j usage 'riotaeqbii' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    riotaeqi.1 $e |- A = B $.
+    $( Equal domains yield equal restricted iotas.  Inference version.
+       (Contributed by GG, 1-Sep-2025.) $)
+    riotaeqi $p |- ( iota_ x e. A ph ) = ( iota_ x e. B ph ) $=
+      ( biid riotaeqbii ) AABCDEAFG $.
+    $( $j usage 'riotaeqi' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d A f $.  $d B f $.  $d C f $.  $d x f $.
+    ixpeq1i.1 $e |- A = B $.
+    $( Equality inference for infinite Cartesian product.  (Contributed by GG,
+       1-Sep-2025.) $)
+    ixpeq1i $p |- X_ x e. A C = X_ x e. B C $=
+      ( vf cv wcel cab wfn cfv wral wa cixp eleq2i fneq2i imbi1i ralbii2 df-ixp
+      abbii anbi12i 3eqtr4i ) FGZAGZBHZAIZJZUDUCKDHZABLZMZFIUCUDCHZAIZJZUHACLZM
+      ZFIABDNACDNUJUOFUGUMUIUNUFULUCUEUKABCUDEOZTPUHUHABCUEUKUHUPQRUATABDFSACDF
+      SUB $.
+    $( $j usage 'ixpeq1i' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    ixpeq12i.1 $e |- A = B $.
+    ixpeq12i.2 $e |- C = D $.
+    $( Equality inference for infinite Cartesian product.  (Contributed by GG,
+       1-Sep-2025.) $)
+    ixpeq12i $p |- X_ x e. A C = X_ x e. B D $=
+      ( cixp wceq wral rgenw ixpeq2 ax-mp ixpeq1i eqtri ) ABDHZABEHZACEHDEIZABJ
+      PQIRABGKABDELMABCEFNO $.
+    $( $j usage 'ixpeq12i' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d A x m n f $.  $d B x m n f $.  $d C x m n f $.  $d k x m n f $.
+    sumeq2si.1 $e |- B = C $.
+    $( Equality inference for sum.  (Contributed by GG, 1-Sep-2025.) $)
+    sumeq2si $p |- sum_ k e. A B = sum_ k e. A C $=
+      ( vm vn vx vf cv cfv caddc cz csb cmpt cseq wa wrex cn wceq cuz wss c1 co
+      wcel cc0 cif cli wbr cfz wf1o wex wo cio csu csbeq2i ifeq1 mpteq2i seqeq3
+      ax-mp breq1i anbi2i rexbii fveq1i eqeq2i orbi12i iotabii df-sum 3eqtr4i
+      exbii ) AFJZUAKUBZLGMGJZAUEZDVMBNZUFUGZOZVKPZHJZUHUIZQZFMRZUCVKUJUDAIJZUK
+      ZVSVKLGSDVMWCKZBNZOZUCPZKZTZQZIULZFSRZUMZHUNVLLGMVNDVMCNZUFUGZOZVKPZVSUHU
+      IZQZFMRZWDVSVKLGSDWECNZOZUCPZKZTZQZIULZFSRZUMZHUNABDUOACDUOWNXJHWBXAWMXIW
+      AWTFMVTWSVLVRWRVSUHVQWQTVRWRTGMVPWPVOWOTVPWPTDVMBCEUPVNVOWOUFUQUTURLVQWQV
+      KUSUTVAVBVCWLXHFSWKXGIWJXFWDWIXEVSVKWHXDWGXCTWHXDTGSWFXBDWEBCEUPURLWGXCUC
+      USUTVDVEVBVJVCVFVGHABIDFGVHHACIDFGVHVI $.
+    $( $j usage 'sumeq2si' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    sumeq12si.1 $e |- A = B $.
+    sumeq12si.2 $e |- C = D $.
+    $( Equality inference for sum.  General version of ~ sumeq2si .
+       (Contributed by GG, 1-Sep-2025.) $)
+    sumeq12si $p |- sum_ x e. A C = sum_ x e. B D $=
+      ( csu sumeq1i sumeq2si eqtri ) BDAHCDAHCEAHBCDAFICDEAGJK $.
+    $( $j usage 'sumeq12si' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d A x m n y f $.  $d B x m n y f $.  $d C x m n y f $.  $d k x m n y f $.
+    prodeq2si.1 $e |- B = C $.
+    $( Equality inference for product.  (Contributed by GG, 1-Sep-2025.) $)
+    prodeq2si $p |- prod_ k e. A B = prod_ k e. A C $=
+      ( vm vy vn vx vf cv cfv cmul cz c1 cseq cli wrex cn wceq cuz wss cc0 wcel
+      wne cif cmpt wbr wa wex w3a cfz co wf1o csb wo cio cprod biid ifeq1 ax-mp
+      mpteq2i seqeq3 breq1i anbi2i exbii rexbii 3anbi123i csbeq2i fveq1i eqeq2i
+      orbi12i iotabii df-prod 3eqtr4i ) AFKZUALZUBZGKZUCUEZMDNDKAUDZBOUFZUGZHKZ
+      PZVSQUHZUIZGUJZHVQRZMWCVPPZIKZQUHZUKZFNRZOVPULUMAJKZUNZWKVPMHSDWDWOLZBUOZ
+      UGZOPZLZTZUIZJUJZFSRZUPZIUQVRVTMDNWACOUFZUGZWDPZVSQUHZUIZGUJZHVQRZMXHVPPZ
+      WKQUHZUKZFNRZWPWKVPMHSDWQCUOZUGZOPZLZTZUIZJUJZFSRZUPZIUQABDURACDURXFYFIWN
+      XQXEYEWMXPFNVRVRWIXMWLXOVRUSWHXLHVQWGXKGWFXJVTWEXIVSQWCXHTZWEXITDNWBXGBCT
+      WBXGTEWABCOUTVAVBZMWCXHWDVCVAVDVEVFVGWJXNWKQYGWJXNTYHMWCXHVPVCVAVDVHVGXDY
+      DFSXCYCJXBYBWPXAYAWKVPWTXTWSXSTWTXTTHSWRXRDWQBCEVIVBMWSXSOVCVAVJVKVEVFVGV
+      LVMIGABJDFHVNIGACJDFHVNVO $.
+    $( $j usage 'prodeq2si' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    prodeq12si.1 $e |- A = B $.
+    prodeq12si.2 $e |- C = D $.
+    $( Equality inference for product.  General version of ~ prodeq2si .
+       (Contributed by GG, 1-Sep-2025.) $)
+    prodeq12si $p |- prod_ x e. A C = prod_ x e. B D $=
+      ( cprod prodeq1i prodeq2si eqtri ) BDAHCDAHCEAHBCDAFICDEAGJK $.
+    $( $j usage 'prodeq12si' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d A k y $.  $d B k y $.  $d C k y $.  $d D k y $.  $d x k y $.
+    itgeq12i.1 $e |- A = B $.
+    itgeq12i.2 $e |- C = D $.
+    $( Equality inference for an integral.  General version of ~ itgeq1i and
+       ~ itgeq2i .  (Contributed by GG, 1-Sep-2025.) $)
+    itgeq12i $p |- S. A C _d x = S. B D _d x $=
+      ( vk vy cc0 co cv cr cdiv cre cfv wa csb citg2 cmul cfz cexp wcel cle wbr
+      c3 ci cif cmpt csu citg wceq wal oveq1i fveq2i eleq2i anbi1i ax-mp ax-gen
+      wb pm3.2i csbeq2 csbeq1 sylan9eqr mpteq2i oveq2i sumeq2si df-itg 3eqtr4i
+      ifbi ) JUFUAKZUGHLUBKZAMIDVLNKZOPZALZBUCZJILZUDUEZQZVQJUHZRZUIZSPZTKZHUJV
+      KVLAMIEVLNKZOPZVOCUCZVRQZVQJUHZRZUIZSPZTKZHUJABDUKACEUKVKWDWMHWCWLVLTWBWK
+      SAMWAWJVNWFULZVTWIULZIUMZQWAWJULWNWPVMWEODEVLNGUNUOWOIVSWHUTWOVPWGVRBCVOF
+      UPUQVSWHVQJVJURUSVAWPWNWAIVNWIRWJIVNVTWIVBIVNWFWIVCVDURVEUOVFVGAIBDHVHAIC
+      EHVHVI $.
+    $( $j usage 'itgeq12i' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    itgeq1i.1 $e |- A = B $.
+    $( Equality inference for an integral.  (Contributed by GG, 1-Sep-2025.) $)
+    itgeq1i $p |- S. A C _d x = S. B C _d x $=
+      ( eqid itgeq12i ) ABCDDEDFG $.
+    $( $j usage 'itgeq1i' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    itgeq2i.1 $e |- B = C $.
+    $( Equality inference for an integral.  (Contributed by GG, 1-Sep-2025.) $)
+    itgeq2i $p |- S. A B _d x = S. A C _d x $=
+      ( eqid itgeq12i ) ABBCDBFEG $.
+    $( $j usage 'itgeq2i' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    ditgeq123i.1 $e |- A = B $.
+    ditgeq123i.2 $e |- C = D $.
+    ditgeq123i.3 $e |- E = F $.
+    $( Equality inference for the directed integral.  General version of
+       ~ ditgeq12i and ~ ditgeq3i .  (Contributed by GG, 1-Sep-2025.) $)
+    ditgeq123i $p |- S_ [ A -> C ] E _d x = S_ [ B -> D ] F _d x $=
+      ( cle wbr cioo co citg cneg cif cdit oveq12i itgeq12i breq12i ifbieq12i
+      negeqi df-ditg 3eqtr4i ) BDKLZABDMNZFOZADBMNZFOZPZQCEKLZACEMNZGOZAECMNZGO
+      ZPZQABDFRACEGRUFULUHUKUNUQBCDEKHIUAAUGUMFGBCDEMHISJTUJUPAUIUOFGDEBCMIHSJT
+      UCUBABDFUDACEGUDUE $.
+   $( $j usage 'ditgeq123i' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    ditgeq12i.1 $e |- A = B $.
+    ditgeq12i.2 $e |- C = D $.
+    $( Equality inference for the directed integral.  (Contributed by GG,
+       1-Sep-2025.) $)
+    ditgeq12i $p |- S_ [ A -> C ] E _d x = S_ [ B -> D ] E _d x $=
+      ( eqid ditgeq123i ) ABCDEFFGHFIJ $.
+    $( $j usage 'ditgeq12i' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    ditgeq3i.1 $e |- C = D $.
+    $( Equality inference for the directed integral.  (Contributed by GG,
+       1-Sep-2025.) $)
+    ditgeq3i $p |- S_ [ A -> B ] C _d x = S_ [ A -> B ] D _d x $=
+      ( eqid ditgeq123i ) ABBCCDEBGCGFH $.
+    $( $j usage 'ditgeq3i' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+
+$(
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+  Deduction versions.
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+$)
+
+  ${
+    $d A x $.  $d B x $.
+    rmoeqdv.1 $e |- ( ph -> A = B ) $.
+    $( Formula-building rule for restricted at-most-one quantifier.  Deduction
+       form.  (Contributed by GG, 1-Sep-2025.) $)
+    rmoeqdv $p |- ( ph -> ( E* x e. A ps <-> E* x e. B ps ) ) $=
+      ( wceq wrmo wb rmoeq1 syl ) ADEGBCDHBCEHIFBCDEJK $.
+    $( $j usage 'rmoeqdv' avoids 'ax-8' 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d ph x $.
+    rmoeqbidv.1 $e |- ( ph -> A = B ) $.
+    rmoeqbidv.2 $e |- ( ph -> ( ps <-> ch ) ) $.
+    $( Formula-building rule for restricted at-most-one quantifier.  Deduction
+       form.  General version of ~ rmobidv .  (Contributed by GG,
+       1-Sep-2025.) $)
+    rmoeqbidv $p |- ( ph -> ( E* x e. A ps <-> E* x e. B ch ) ) $=
+      ( cv wcel wa wmo wrmo eleq2d anbi12d mobidv df-rmo 3bitr4g ) ADIZEJZBKZDL
+      SFJZCKZDLBDEMCDFMAUAUCDATUBBCAEFSGNHOPBDEQCDFQR $.
+    $( $j usage 'rmoeqbidv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d A x $.  $d B x $.
+    reueqdv.1 $e |- ( ph -> A = B ) $.
+    $( Formula-building rule for restricted existential uniqueness quantifier.
+       Deduction form.  (Contributed by GG, 1-Sep-2025.) $)
+    reueqdv $p |- ( ph -> ( E! x e. A ps <-> E! x e. B ps ) ) $=
+      ( wceq wreu wb reueq1 syl ) ADEGBCDHBCEHIFBCDEJK $.
+    $( $j usage 'reueqdv' avoids 'ax-8' 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d ph x $.
+    reueqbidv.1 $e |- ( ph -> A = B ) $.
+    reueqbidv.2 $e |- ( ph -> ( ps <-> ch ) ) $.
+    $( Formula-building rule for restricted existential uniqueness quantifier.
+       Deduction form.  General version of ~ reubidv .  (Contributed by GG,
+       1-Sep-2025.) $)
+    reueqbidv $p |- ( ph -> ( E! x e. A ps <-> E! x e. B ch ) ) $=
+      ( cv wcel wa weu wreu eleq2d anbi12d eubidv df-reu 3bitr4g ) ADIZEJZBKZDL
+      SFJZCKZDLBDEMCDFMAUAUCDATUBBCAEFSGNHOPBDEQCDFQR $.
+    $( $j usage 'reueqbidv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d ph x t $.  $d ps t $.  $d ch t $.  $d t u $.  $d t v $.
+    sbequbidv.1 $e |- ( ph -> u = v ) $.
+    sbequbidv.2 $e |- ( ph -> ( ps <-> ch ) ) $.
+    $( Deduction substituting both sides of a biconditional.  (Contributed by
+       GG, 1-Sep-2025.) $)
+    sbequbidv $p |- ( ph -> ( [ u / x ] ps <-> [ v / x ] ch ) ) $=
+      ( vt weq wi wal wsb wb equequ2 syl imbi2d albidv imbi12d df-sb 3bitr4g )
+      AIFJZDIJZBKZDLZKZILIEJZUCCKZDLZKZILBDFMCDEMAUFUJIAUBUGUEUIAFEJUBUGNGFEIOP
+      AUDUHDABCUCHQRSRBDIFTCDIETUA $.
+    $( $j usage 'sbequbidv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d ph x t $.  $d A t $.  $d B t $.  $d C t $.
+    disjeq12dv.1 $e |- ( ph -> A = B ) $.
+    disjeq12dv.2 $e |- ( ph -> C = D ) $.
+    $( Equality theorem for disjoint collection.  Deduction version.
+       (Contributed by GG, 1-Sep-2025.) $)
+    disjeq12dv $p |- ( ph -> ( Disj_ x e. A C <-> Disj_ x e. B D ) ) $=
+      ( vt wdisj cv wcel wrmo wal wa wmo eleq2d df-rmo 3bitr4g df-disj anbi1d
+      mobidv albidv wceq adantr disjeq2dv bitrd ) ABCEJZBDEJZBDFJAIKELZBCMZINUJ
+      BDMZINUHUIAUKULIABKZCLZUJOZBPUMDLZUJOZBPUKULAUOUQBAUNUPUJACDUMGQUAUBUJBCR
+      UJBDRSUCBICETBIDETSABDEFAEFUDUPHUEUFUG $.
+    $( $j usage 'disjeq12dv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d ph x t $.  $d A t $.  $d B t $.  $d C t $.
+    ixpeq12dv.1 $e |- ( ph -> A = B ) $.
+    ixpeq12dv.2 $e |- ( ph -> C = D ) $.
+    $( Equality theorem for infinite Cartesian product.  Deduction version.
+       (Contributed by GG, 1-Sep-2025.) $)
+    ixpeq12dv $p |- ( ph -> X_ x e. A C = X_ x e. B D ) $=
+      ( vt cixp cv wcel cab wfn wral wa abbidv wi wal df-ral cfv eleq2d 3bitr4g
+      fneq2d imbi1d albidv anbi12d df-ixp 3eqtr4g ixpeq2dv eqtrd ) ABCEJZBDEJZB
+      DFJAIKZBKZCLZBMZNZUOUNUAELZBCOZPZIMUNUODLZBMZNZUSBDOZPZIMULUMAVAVFIAURVDU
+      TVEAUQVCUNAUPVBBACDUOGUBZQUDAUPUSRZBSVBUSRZBSUTVEAVHVIBAUPVBUSVGUEUFUSBCT
+      USBDTUCUGQBCEIUHBDEIUHUIABDEFHUJUK $.
+    $( $j usage 'ixpeq12dv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d ph k $.
+    sumeq12sdv.1 $e |- ( ph -> A = B ) $.
+    sumeq12sdv.2 $e |- ( ph -> C = D ) $.
+    $( Equality deduction for sum.  General version of ~ sumeq2sdv .
+       (Contributed by GG, 1-Sep-2025.) $)
+    sumeq12sdv $p |- ( ph -> sum_ k e. A C = sum_ k e. B D ) $=
+      ( csu sumeq1d sumeq2sdv eqtrd ) ABDFICDFICEFIABCDFGJACDEFHKL $.
+    $( $j usage 'sumeq12sdv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d A x m n y f $.  $d B x m n y f $.  $d C x m n y f $.
+    $d ph k x m n y f $.
+    prodeq12sdv.1 $e |- ( ph -> A = B ) $.
+    prodeq12sdv.2 $e |- ( ph -> C = D ) $.
+    $( Equality deduction for product.  General version of ~ prodeq2sdv .
+       (Contributed by GG, 1-Sep-2025.) $)
+    prodeq12sdv $p |- ( ph -> prod_ k e. A C = prod_ k e. B D ) $=
+      ( vm vy vn vx vf cv cmul cz c1 cseq cli wrex cuz cfv wss cc0 wne wcel cif
+      cprod cmpt wbr wa wex w3a cfz co wf1o cn csb wceq cio sseq1d eleq2d ifbid
+      wo mpteq2dv seqeq3d breq1d anbi2d exbidv rexbidv 3anbi123d f1oeq3d anbi1d
+      orbi12d iotabidv df-prod 3eqtr4g prodeq2sdv eqtrd ) ABDFUHZCDFUHZCEFUHABI
+      NZUAUBZUCZJNZUDUEZOFPFNZBUFZDQUGZUIZKNZRZWESUJZUKZJULZKWCTZOWJWBRZLNZSUJZ
+      UMZIPTZQWBUNUOZBMNZUPZWRWBOKUQFWKXCUBDURUIQRUBUSZUKZMULZIUQTZVDZLUTCWCUCZ
+      WFOFPWGCUFZDQUGZUIZWKRZWESUJZUKZJULZKWCTZOXMWBRZWRSUJZUMZIPTZXBCXCUPZXEUK
+      ZMULZIUQTZVDZLUTVTWAAXIYGLAXAYBXHYFAWTYAIPAWDXJWPXRWSXTABCWCGVAAWOXQKWCAW
+      NXPJAWMXOWFAWLXNWESAWJXMOWKAFPWIXLAWHXKDQABCWGGVBVCVEZVFVGVHVIVJAWQXSWRSA
+      WJXMOWBYHVFVGVKVJAXGYEIUQAXFYDMAXDYCXEABCXBXCGVLVMVIVJVNVOLJBDMFIKVPLJCDM
+      FIKVPVQACDEFHVRVS $.
+    $( $j usage 'prodeq12sdv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d ph x $.  $d A k y $.  $d B k y $.  $d C k y $.  $d D k y $.
+    $d ph x k y $.
+    itgeq12sdv.1 $e |- ( ph -> A = B ) $.
+    itgeq12sdv.2 $e |- ( ph -> C = D ) $.
+    $( Equality theorem for an integral.  Deduction form.  General version of
+       ~ itgeq1d and ~ itgeq2sdv .  (Contributed by GG, 1-Sep-2025.) $)
+    itgeq12sdv $p |- ( ph -> S. A C _d x = S. B D _d x ) $=
+      ( vk vy cc0 co cv cr cdiv cre cfv wcel citg2 cmul c3 cfz cexp cle wbr cif
+      ci csb cmpt csu citg oveq1d fveq2d eleq2d anbi1d ifbid csbeq12dv mpteq2dv
+      wa oveq2d sumeq2sdv df-itg 3eqtr4g ) AKUAUBLZUGIMUCLZBNJEVEOLZPQZBMZCRZKJ
+      MZUDUEZUSZVJKUFZUHZUIZSQZTLZIUJVDVEBNJFVEOLZPQZVHDRZVKUSZVJKUFZUHZUIZSQZT
+      LZIUJBCEUKBDFUKAVDVQWFIAVPWEVETAVOWDSABNVNWCAJVGVMVSWBAVFVRPAEFVEOHULUMAV
+      LWAVJKAVIVTVKACDVHGUNUOUPUQURUMUTVABJCEIVBBJDFIVBVC $.
+    $( $j usage 'itgeq12sdv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d ph x $.
+    itgeq2sdv.1 $e |- ( ph -> B = C ) $.
+    $( Equality theorem for an integral.  Deduction form.  (Contributed by GG,
+       1-Sep-2025.) $)
+    itgeq2sdv $p |- ( ph -> S. A B _d x = S. A C _d x ) $=
+      ( eqidd itgeq12sdv ) ABCCDEACGFH $.
+    $( $j usage 'itgeq2sdv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d ph x $.
+    ditgeq123dv.1 $e |- ( ph -> A = B ) $.
+    ditgeq123dv.2 $e |- ( ph -> C = D ) $.
+    ditgeq123dv.3 $e |- ( ph -> E = F ) $.
+    $( Equality theorem for the directed integral.  Deduction form.  General
+       version of ~ ditgeq3sdv .  (Contributed by GG, 1-Sep-2025.) $)
+    ditgeq123dv $p |- ( ph -> S_ [ A -> C ] E _d x = S_ [ B -> D ] F _d x ) $=
+      ( cle wbr cioo co citg cneg cif cdit oveq12d breq12d itgeq12sdv ifbieq12d
+      negeqd df-ditg 3eqtr4g ) ACELMZBCENOZGPZBECNOZGPZQZRDFLMZBDFNOZHPZBFDNOZH
+      PZQZRBCEGSBDFHSAUGUMUIULUOURACDEFLIJUAABUHUNGHACDEFNIJTKUBAUKUQABUJUPGHAE
+      FCDNJITKUBUDUCBCEGUEBDFHUEUF $.
+    $( $j usage 'ditgeq123dv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d A x $.  $d B x $.  $d C x $.  $d D x $.
+    ditgeq12d.1 $e |- ( ph -> A = B ) $.
+    ditgeq12d.2 $e |- ( ph -> C = D ) $.
+    $( Equality theorem for the directed integral.  Deduction form.
+       (Contributed by GG, 1-Sep-2025.) $)
+    ditgeq12d $p |- ( ph -> S_ [ A -> C ] E _d x = S_ [ B -> D ] E _d x ) $=
+      ( wceq cdit ditgeq1 ditgeq2 sylan9eq syl2anc ) ACDJZEFJZBCEGKZBDFGKZJHIPQ
+      RBDEGKSBCDEGLBEFDGMNO $.
+    $( $j usage 'ditgeq12d' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d ph x $.
+    ditgeq3sdv.1 $e |- ( ph -> C = D ) $.
+    $( Equality theorem for the directed integral.  Deduction form.
+       (Contributed by GG, 1-Sep-2025.) $)
+    ditgeq3sdv $p |- ( ph -> S_ [ A -> B ] C _d x = S_ [ A -> B ] D _d x ) $=
+      ( eqidd ditgeq123dv ) ABCCDDEFACHADHGI $.
+    $( $j usage 'ditgeq3sdv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
   Change bound variables.
@@ -578615,6 +579209,32 @@ conditions of the Five Segment Axiom ( ~ ax5seg ).  See ~ brofs and
     $( $j usage 'cbvreuvw2' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
   $}
 
+  ${
+    $d x y $.  $d ph y $.  $d ps x $.
+    cbvsbcvw2.1 $e |- A = B $.
+    cbvsbcvw2.2 $e |- ( x = y -> ( ph <-> ps ) ) $.
+    $( Change bound variable of a class substitution using implicit
+       substitution.  General version of ~ cbvsbcvw .  (Contributed by GG,
+       1-Sep-2025.) $)
+    cbvsbcvw2 $p |- ( [. A / x ]. ph <-> [. B / y ]. ps ) $=
+      ( cab wcel wsbc cbvabv eleq12i df-sbc 3bitr4i ) EACIZJFBDIZJACEKBDFKEFPQG
+      ABCDHLMACENBDFNO $.
+    $( $j usage 'cbvsbcvw2' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d x y $.  $d A t $.  $d B t $.  $d C y t $.  $d D x t $.
+    cbvcsbvw2.1 $e |- A = B $.
+    cbvcsbvw2.2 $e |- ( x = y -> C = D ) $.
+    $( Change bound variable of a proper substitution into a class using
+       implicit substitution.  General version of ~ cbvcsbv .  (Contributed by
+       GG, 1-Sep-2025.) $)
+    cbvcsbvw2 $p |- [_ A / x ]_ C = [_ B / y ]_ D $=
+      ( vt cv wcel wsbc cab csb weq eleq2d cbvsbcvw2 abbii df-csb 3eqtr4i ) IJZ
+      EKZACLZIMUAFKZBDLZIMACENBDFNUCUEIUBUDABCDGABOEFUAHPQRAICESBIDFST $.
+    $( $j usage 'cbvcsbvw2' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
   ${
     $d x y $.  $d A y t $.  $d B x t $.  $d C y t $.  $d D x t $.
     cbviunvw2.1 $e |- ( x = y -> C = D ) $.
@@ -578813,6 +579433,41 @@ conditions of the Five Segment Axiom ( ~ ax5seg ).  See ~ brofs and
     $( $j usage 'cbvixpvw2' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
   $}
 
+  ${
+    $d j k $.  $d D j $.  $d C k $.
+    cbvsumvw2.1 $e |- A = B $.
+    cbvsumvw2.2 $e |- ( j = k -> C = D ) $.
+    $( Change bound variable and the set of integers in a sum, using implicit
+       substitution.  (Contributed by GG, 1-Sep-2025.) $)
+    cbvsumvw2 $p |- sum_ j e. A C = sum_ k e. B D $=
+      ( csu cbvsumv sumeq1i eqtri ) ACEIADFIBDFIACDEFHJABDFGKL $.
+    $( $j usage 'cbvsumvw2' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d j k x y m n f $.  $d D j x y m n f $.  $d C k x y m n f $.
+    $d A k x y m n f $.  $d B j x y m n f $.
+    cbvprodvw2.1 $e |- A = B $.
+    cbvprodvw2.2 $e |- ( j = k -> C = D ) $.
+    $( Change bound variable and the set of integers in a product, using
+       implicit substitution.  (Contributed by GG, 1-Sep-2025.) $)
+    cbvprodvw2 $p |- prod_ j e. A C = prod_ k e. B D $=
+      ( vm vy vn vx vf cv cmul cz c1 cseq cli wceq cuz cfv wss cc0 wne wcel cif
+      cmpt wbr wa wex wrex w3a cfz co wf1o cn csb wo cprod sseq1i eleq2i eleq1w
+      cio weq bitrid ifbieq1d seqeq3 ax-mp breq1i anbi2i exbii rexbii 3anbi123i
+      cbvmptv wb f1oeq3 cbvcsbv mpteq2i anbi12i orbi12i iotabii df-prod 3eqtr4i
+      fveq1i eqeq2i ) AINZUAUBZUCZJNZUDUEZOEPENZAUFZCQUGZUHZKNZRZWJSUIZUJZJUKZK
+      WHULZOWOWGRZLNZSUIZUMZIPULZQWGUNUOZAMNZUPZXCWGOKUQEWPXHUBZCURZUHZQRZUBZTZ
+      UJZMUKZIUQULZUSZLVDBWHUCZWKOFPFNBUFZDQUGZUHZWPRZWJSUIZUJZJUKZKWHULZOYCWGR
+      ZXCSUIZUMZIPULZXGBXHUPZXCWGOKUQFXJDURZUHZQRZUBZTZUJZMUKZIUQULZUSZLVDACEUT
+      BDFUTXSUUBLXFYLXRUUAXEYKIPWIXTXAYHXDYJABWHGVAWTYGKWHWSYFJWRYEWKWQYDWJSWOY
+      CTZWQYDTEFPWNYBEFVEZWMYACDQWMWLBUFUUDYAABWLGVBEFBVCVFHVGVOZOWOYCWPVHVIVJV
+      KVLVMXBYIXCSUUCXBYITUUEOWOYCWGVHVIVJVNVMXQYTIUQXPYSMXIYMXOYRABTXIYMVPGABX
+      GXHVQVIXNYQXCWGXMYPXLYOTXMYPTKUQXKYNEFXJCDHVRVSOXLYOQVHVIWEWFVTVLVMWAWBLJ
+      ACMEIKWCLJBDMFIKWCWD $.
+    $( $j usage 'cbvprodvw2' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
   ${
     $d x y $.  $d A y t v $.  $d B x t v $.  $d C y t v $.  $d D x t v $.
     cbvitgvw2.1 $e |- ( x = y -> C = D ) $.
@@ -578821,15 +579476,30 @@ conditions of the Five Segment Axiom ( ~ ax5seg ).  See ~ brofs and
        substitution.  (Contributed by GG, 14-Aug-2025.) $)
     cbvitgvw2 $p |- S. A C _d x = S. B D _d y $=
       ( vt vv cc0 co cv cr cdiv cre cfv wcel citg2 cmul c3 cfz cexp cle wbr cif
-      ci wa csb cmpt csu citg wceq wtru weq fvoveq1d id eleq12d ifbid csbeq12dv
-      anbi1d cbvmptv fveq2i oveq2i a1i sumeq2sdv mptru df-itg 3eqtr4i ) KUAUBLZ
-      UGIMUCLZANJEVKOLPQZAMZCRZKJMZUDUEZUHZVOKUFZUIZUJZSQZTLZIUKZVJVKBNJFVKOLPQ
-      ZBMZDRZVPUHZVOKUFZUIZUJZSQZTLZIUKZACEULBDFULWCWMUMUNVJWBWLIWBWLUMUNWAWKVK
-      TVTWJSABNVSWIABUOZJVLVRWDWHWNEFVKPOGUPWNVQWGVOKWNVNWFVPWNVMWECDWNUQHURVAU
-      SUTVBVCVDVEVFVGAJCEIVHBJDFIVHVI $.
+      ci wa csb cmpt csu weq fvoveq1d id eleq12d anbi1d ifbid csbeq12dv cbvmptv
+      citg fveq2i oveq2i sumeq2si df-itg 3eqtr4i ) KUAUBLZUGIMUCLZANJEVGOLPQZAM
+      ZCRZKJMZUDUEZUHZVKKUFZUIZUJZSQZTLZIUKVFVGBNJFVGOLPQZBMZDRZVLUHZVKKUFZUIZU
+      JZSQZTLZIUKACEUTBDFUTVFVRWGIVQWFVGTVPWESABNVOWDABULZJVHVNVSWCWHEFVGPOGUMW
+      HVMWBVKKWHVJWAVLWHVIVTCDWHUNHUOUPUQURUSVAVBVCAJCEIVDBJDFIVDVE $.
     $( $j usage 'cbvitgvw2' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
   $}
 
+  ${
+    $d x y $.  $d A y $.  $d B x $.  $d C y $.  $d D x $.  $d E y $.  $d F x $.
+    cbvditgvw2.1 $e |- A = B $.
+    cbvditgvw2.2 $e |- C = D $.
+    cbvditgvw2.3 $e |- ( x = y -> E = F ) $.
+    $( Change bound variable and domain in a directed integral, using implicit
+       substitution.  (Contributed by GG, 1-Sep-2025.) $)
+    cbvditgvw2 $p |- S_ [ A -> C ] E _d x = S_ [ B -> D ] F _d y $=
+      ( cle wbr cioo co citg cneg cif wceq a1i cdit breq12i weq oveq12i oveq12d
+      cbvitgvw2 negeqi ifbieq12i df-ditg 3eqtr4i ) CELMZACENOZGPZAECNOZGPZQZRDF
+      LMZBDFNOZHPZBFDNOZHPZQZRACEGUABDFHUAUKUQUMUPUSVBCDEFLIJUBABULURGHKULURSAB
+      UCZCDEFNIJUDTUFUOVAABUNUTGHKVCEFCDNEFSVCJTCDSVCITUEUFUGUHACEGUIBDFHUIUJ
+      $.
+    $( $j usage 'cbvditgvw2' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
 
 $(
 -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
@@ -579336,8 +580006,8 @@ conditions of the Five Segment Axiom ( ~ ax5seg ).  See ~ brofs and
     $d ph x y t $.  $d A y t $.  $d B x t $.  $d C y t $.  $d D x t $.
     cbviundavw2.1 $e |- ( ( ph /\ x = y ) -> C = D ) $.
     cbviundavw2.2 $e |- ( ( ph /\ x = y ) -> A = B ) $.
-    $( Change bound variable in indexed unions.  Deduction form.  (Contributed
-       by GG, 14-Aug-2025.) $)
+    $( Change bound variable and domain in indexed unions.  Deduction form.
+       (Contributed by GG, 14-Aug-2025.) $)
     cbviundavw2 $p |- ( ph -> U_ x e. A C = U_ y e. B D ) $=
       ( vt cv wcel wrex cab ciun weq wa eleq2d cbvrexdva2 df-iun abbidv 3eqtr4g
       ) AJKZFLZBDMZJNUCGLZCEMZJNBDFOCEGOAUEUGJAUDUFBCDEABCPQFGUCHRISUABJDFTCJEG
@@ -579349,8 +580019,8 @@ conditions of the Five Segment Axiom ( ~ ax5seg ).  See ~ brofs and
     $d ph x y t $.  $d A y t $.  $d B x t $.  $d C y t $.  $d D x t $.
     cbviindavw2.1 $e |- ( ( ph /\ x = y ) -> C = D ) $.
     cbviindavw2.2 $e |- ( ( ph /\ x = y ) -> A = B ) $.
-    $( Change bound variable in indexed intersections.  Deduction form.
-       (Contributed by GG, 14-Aug-2025.) $)
+    $( Change bound variable and domain in indexed intersections.  Deduction
+       form.  (Contributed by GG, 14-Aug-2025.) $)
     cbviindavw2 $p |- ( ph -> |^|_ x e. A C = |^|_ y e. B D ) $=
       ( vt cv wcel wral cab ciin weq wa eleq2d cbvraldva2 df-iin abbidv 3eqtr4g
       ) AJKZFLZBDMZJNUCGLZCEMZJNBDFOCEGOAUEUGJAUDUFBCDEABCPQFGUCHRISUABJDFTCJEG
@@ -744089,12 +744759,13 @@ unification theorem (e.g., the sub-theorem whose assertion is step 5
   $}
 
   ${
-    $d A x $.  $d B x $.
+    $d t x $.  $d A t $.  $d B t $.  $d C t $.
     iuneq1i.1 $e |- A = B $.
     $( Equality theorem for indexed union.  (Contributed by Glauco Siliprandi,
-       3-Mar-2021.) $)
+       3-Mar-2021.)  Remove DV conditions.  (Revised by GG, 1-Sep-2025.) $)
     iuneq1i $p |- U_ x e. A C = U_ x e. B C $=
-      ( wceq ciun iuneq1 ax-mp ) BCFABDGACDGFEABCDHI $.
+      ( vt cv wcel wrex cab ciun eleq2i anbi1i rexbii2 abbii df-iun 3eqtr4i ) F
+      GDHZABIZFJRACIZFJABDKACDKSTFRRABCAGZBHUACHRBCUAELMNOAFBDPAFCDPQ $.
   $}
 
   ${
@@ -744360,13 +745031,17 @@ unification theorem (e.g., the sub-theorem whose assertion is step 5
   $}
 
   ${
-    $d A x $.  $d B x $.  $d ph x $.
+    $d A t $.  $d B t $.  $d C t $.  $d ph x t $.
     iineq12dv.1 $e |- ( ph -> A = B ) $.
     iineq12dv.2 $e |- ( ( ph /\ x e. B ) -> C = D ) $.
     $( Equality deduction for indexed intersection.  (Contributed by Glauco
-       Siliprandi, 26-Jun-2021.) $)
+       Siliprandi, 26-Jun-2021.)  Remove DV conditions.  (Revised by GG,
+       1-Sep-2025.) $)
     iineq12dv $p |- ( ph -> |^|_ x e. A C = |^|_ x e. B D ) $=
-      ( ciin iineq1d iineq2dv eqtrd ) ABCEIBDEIBDFIABCDEGJABDEFHKL $.
+      ( vt ciin cv wcel wral cab eleq2d imbi1d ralbidv2 abbidv df-iin 3eqtr4g
+      iineq2dv eqtrd ) ABCEJZBDEJZBDFJAIKELZBCMZINUEBDMZINUCUDAUFUGIAUEUEBCDABK
+      ZCLUHDLUEACDUHGOPQRBICESBIDESTABDEFHUAUB $.
+    $( $j usage 'iineq12dv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
   $}
 
   ${
@@ -762552,6 +763227,7 @@ distinct definitions for the same symbol (limit of a sequence).
        11-Dec-2019.) $)
     itgeq1d $p |- ( ph -> S. A C _d x = S. B C _d x ) $=
       ( wceq citg itgeq1 syl ) ACDGBCEHBDEHGFBCDEIJ $.
+    $( $j usage 'itgeq1d' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
   $}
 
   ${

From 86ebd48ecaca9c689c207a90c686350eb6761373 Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Mon, 1 Sep 2025 18:32:56 +0200
Subject: [PATCH 2/3] tweaks

---
 set.mm | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/set.mm b/set.mm
index 0e58bf06b0..af4c4fc71f 100644
--- a/set.mm
+++ b/set.mm
@@ -177961,6 +177961,7 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/
     $( Equality inference for sum.  (Contributed by NM, 2-Jan-2006.) $)
     sumeq1i $p |- sum_ k e. A C = sum_ k e. B C $=
       ( wceq csu sumeq1 ax-mp ) ABFACDGBCDGFEABCDHI $.
+    $( $j usage 'sumeq1i' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
   $}
 
   ${
@@ -177985,6 +177986,7 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/
     $( Equality deduction for sum.  (Contributed by NM, 1-Nov-2005.) $)
     sumeq1d $p |- ( ph -> sum_ k e. A C = sum_ k e. B C ) $=
       ( wceq csu sumeq1 syl ) ABCGBDEHCDEHGFBCDEIJ $.
+    $( $j usage 'sumeq1i' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
   $}
 
   ${
@@ -183368,6 +183370,7 @@ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/
       FMVSXEWKXMWNXOABVREUSWJXLHVRWIXKGWHXJWAWGXIVTPWEXHTZWGXITDMWDXGWCXFUTWDXG
       TABWBEVAWCXFCNVLVBVCZLWEXHWFVDVBVEVFVMVGWLXNWMPYCWLXNTYDLWEXHVQVDVBVEVHVG
       XBXTFUNXAXSJWSXRWTABTWSXRUTEABWQWRVIVBVJVMVGVKVNIGACJDFHVOIGBCJDFHVOVP $.
+    $( $j usage 'prodeq1i' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
   $}
 
   ${
@@ -579783,8 +579786,7 @@ conditions of the Five Segment Axiom ( ~ ax5seg ).  See ~ brofs and
   $}
 
   ${
-    $d ph x $.  $d A k y $.  $d B k y $.  $d C k y $.  $d D k y $.
-    $d ph x k y $.
+    $d ph x k y $.  $d A k y $.  $d B k y $.  $d C k y $.  $d D k y $.
     itgeq12sdv.1 $e |- ( ph -> A = B ) $.
     itgeq12sdv.2 $e |- ( ph -> C = D ) $.
     $( Equality theorem for an integral.  Deduction form.  General version of
@@ -745888,6 +745890,7 @@ unification theorem (e.g., the sub-theorem whose assertion is step 5
     iuneq1i $p |- U_ x e. A C = U_ x e. B C $=
       ( vt cv wcel wrex cab ciun eleq2i anbi1i rexbii2 abbii df-iun 3eqtr4i ) F
       GDHZABIZFJRACIZFJABDKACDKSTFRRABCAGZBHUACHRBCUAELMNOAFBDPAFCDPQ $.
+    $( $j usage 'iuneq1i' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
   $}
 
   ${

From 65b1e1ac63ac47b6cae2d4e4ae341bf6c1747ad1 Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Mon, 1 Sep 2025 18:34:51 +0200
Subject: [PATCH 3/3] typo

---
 set.mm | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/set.mm b/set.mm
index af4c4fc71f..089a4d089d 100644
--- a/set.mm
+++ b/set.mm
@@ -177986,7 +177986,7 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/
     $( Equality deduction for sum.  (Contributed by NM, 1-Nov-2005.) $)
     sumeq1d $p |- ( ph -> sum_ k e. A C = sum_ k e. B C ) $=
       ( wceq csu sumeq1 syl ) ABCGBDEHCDEHGFBCDEIJ $.
-    $( $j usage 'sumeq1i' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+    $( $j usage 'sumeq1d' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
   $}
 
   ${