shorten proofs (#4698)

* shorten cbvralsvw * shorten cbvresvw * add tag * typos * discouraged * revise raleq and friends * fix proof of raleq
metamath · Mar 9, 2025 · 20bf817 · 20bf817
1 parent 88170c2
commit 20bf817
Show file tree

Hide file tree

Showing 2 changed files with 119 additions and 60 deletions.
diff --git a/discouraged b/discouraged
@@ -15362,6 +15362,7 @@ New usage of "cbvralcsf" is discouraged (2 uses).
 New usage of "cbvralf" is discouraged (2 uses).
 New usage of "cbvralfwOLD" is discouraged (0 uses).
 New usage of "cbvralsv" is discouraged (0 uses).
+New usage of "cbvralsvwOLD" is discouraged (0 uses).
 New usage of "cbvralv" is discouraged (2 uses).
 New usage of "cbvralv2" is discouraged (1 uses).
 New usage of "cbvreu" is discouraged (2 uses).
@@ -15375,6 +15376,7 @@ New usage of "cbvrexcsf" is discouraged (1 uses).
 New usage of "cbvrexdva2OLD" is discouraged (0 uses).
 New usage of "cbvrexf" is discouraged (1 uses).
 New usage of "cbvrexsv" is discouraged (1 uses).
+New usage of "cbvrexsvwOLD" is discouraged (0 uses).
 New usage of "cbvrexv" is discouraged (2 uses).
 New usage of "cbvrexv2" is discouraged (0 uses).
 New usage of "cbvriota" is discouraged (1 uses).
@@ -18753,6 +18755,8 @@ New usage of "ralcom2" is discouraged (0 uses).
 New usage of "ralcom3OLD" is discouraged (0 uses).
 New usage of "ralcom4OLD" is discouraged (0 uses).
 New usage of "raleleqALT" is discouraged (0 uses).
+New usage of "raleqOLD" is discouraged (0 uses).
+New usage of "raleqbidvvOLD" is discouraged (0 uses).
 New usage of "ralf0OLD" is discouraged (0 uses).
 New usage of "ralidmOLD" is discouraged (0 uses).
 New usage of "ralprgOLD" is discouraged (0 uses).
@@ -18840,6 +18844,8 @@ New usage of "rexbidvALT" is discouraged (0 uses).
 New usage of "rexbidvaALT" is discouraged (0 uses).
 New usage of "rexcomOLD" is discouraged (0 uses).
 New usage of "rexdif1enOLD" is discouraged (0 uses).
+New usage of "rexeqOLD" is discouraged (0 uses).
+New usage of "rexeqbidvvOLD" is discouraged (0 uses).
 New usage of "reximdvaiOLD" is discouraged (0 uses).
 New usage of "reximiaOLD" is discouraged (0 uses).
 New usage of "rexlimddvcbv" is discouraged (0 uses).
@@ -20109,9 +20115,11 @@ Proof modification of "cbvmptvOLD" is discouraged (13 steps).
 Proof modification of "cbvopab1vOLD" is discouraged (13 steps).
 Proof modification of "cbvopabvOLD" is discouraged (20 steps).
 Proof modification of "cbvralfwOLD" is discouraged (139 steps).
+Proof modification of "cbvralsvwOLD" is discouraged (53 steps).
 Proof modification of "cbvreuvwOLD" is discouraged (13 steps).
 Proof modification of "cbvreuwOLD" is discouraged (145 steps).
 Proof modification of "cbvrexdva2OLD" is discouraged (109 steps).
+Proof modification of "cbvrexsvwOLD" is discouraged (53 steps).
 Proof modification of "cbvriotavwOLD" is discouraged (13 steps).
 Proof modification of "cbvrmowOLD" is discouraged (58 steps).
 Proof modification of "ccat2s1fvwALT" is discouraged (116 steps).
@@ -21186,6 +21194,8 @@ Proof modification of "ralcom13OLD" is discouraged (58 steps).
 Proof modification of "ralcom3OLD" is discouraged (38 steps).
 Proof modification of "ralcom4OLD" is discouraged (63 steps).
 Proof modification of "raleleqALT" is discouraged (26 steps).
+Proof modification of "raleqOLD" is discouraged (11 steps).
+Proof modification of "raleqbidvvOLD" is discouraged (98 steps).
 Proof modification of "ralf0OLD" is discouraged (41 steps).
 Proof modification of "ralidmOLD" is discouraged (68 steps).
 Proof modification of "ralprgOLD" is discouraged (17 steps).
@@ -21254,6 +21264,8 @@ Proof modification of "rexbidvALT" is discouraged (10 steps).
 Proof modification of "rexbidvaALT" is discouraged (10 steps).
 Proof modification of "rexcomOLD" is discouraged (67 steps).
 Proof modification of "rexdif1enOLD" is discouraged (120 steps).
+Proof modification of "rexeqOLD" is discouraged (11 steps).
+Proof modification of "rexeqbidvvOLD" is discouraged (47 steps).
 Proof modification of "reximdvaiOLD" is discouraged (28 steps).
 Proof modification of "reximiaOLD" is discouraged (21 steps).
 Proof modification of "rexlimivOLD" is discouraged (23 steps).

diff --git a/set.mm b/set.mm
@@ -30710,27 +30710,39 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
   $}
 
   ${
-    $d z x A $.  $d y A $.  $d z y ph $.  $d x y $.
+    $d x y A $.  $d y ph $.
     $( Change bound variable by using a substitution.  Version of ~ cbvralsv
        with a disjoint variable condition, which does not require ~ ax-13 .
        (Contributed by NM, 20-Nov-2005.)  Avoid ~ ax-13 .  (Revised by Gino
-       Giotto, 10-Jan-2024.) $)
+       Giotto, 10-Jan-2024.)  (Proof shortened by Wolf Lammen, 8-Mar-2025.) $)
     cbvralsvw $p |- ( A. x e. A ph <-> A. y e. A [ y / x ] ph ) $=
-      ( vz wral wsb nfv nfs1v sbequ12 cbvralw sbequ bitri ) ABDFABEGZEDFABCGZCD
-      FANBEDAEHABEIABEJKNOECDNCHOEHAECBLKM $.
+      ( wsb nfv nfs1v sbequ12 cbvralw ) AABCEBCDACFABCGABCHI $.
     $( $j usage 'cbvralsvw' avoids 'ax-13'; $)
-  $}
 
-  ${
-    $d z x A $.  $d y z ph $.  $d y A $.  $d x y $.
     $( Change bound variable by using a substitution.  Version of ~ cbvrexsv
        with a disjoint variable condition, which does not require ~ ax-13 .
        (Contributed by NM, 2-Mar-2008.)  Avoid ~ ax-13 .  (Revised by Gino
-       Giotto, 10-Jan-2024.) $)
+       Giotto, 10-Jan-2024.)  (Proof shortened by Wolf Lammen, 8-Mar-2025.) $)
     cbvrexsvw $p |- ( E. x e. A ph <-> E. y e. A [ y / x ] ph ) $=
+      ( wsb nfv nfs1v sbequ12 cbvrexw ) AABCEBCDACFABCGABCHI $.
+    $( $j usage 'cbvrexsvw' avoids 'ax-13'; $)
+  $}
+
+  ${
+    $d z x A $.  $d y A $.  $d z y ph $.  $d x y $.
+    $( Obsolete version of ~ cbvralsvw as of 8-Mar-2025.  (Contributed by NM,
+       20-Nov-2005.)  Avoid ~ ax-13 .  (Revised by Gino Giotto, 10-Jan-2024.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    cbvralsvwOLD $p |- ( A. x e. A ph <-> A. y e. A [ y / x ] ph ) $=
+      ( vz wral wsb nfv nfs1v sbequ12 cbvralw sbequ bitri ) ABDFABEGZEDFABCGZCD
+      FANBEDAEHABEIABEJKNOECDNCHOEHAECBLKM $.
+
+    $( Obsolete version of ~ cbvrexsvw as of 8-Mar-2025.  (Contributed by NM,
+       20-Nov-2005.)  Avoid ~ ax-13 .  (Revised by Gino Giotto, 10-Jan-2024.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    cbvrexsvwOLD $p |- ( E. x e. A ph <-> E. y e. A [ y / x ] ph ) $=
       ( vz wrex wsb nfv nfs1v sbequ12 cbvrexw sbequ bitri ) ABDFABEGZEDFABCGZCD
       FANBEDAEHABEIABEJKNOECDNCHOEHAECBLKM $.
-    $( $j usage 'cbvrexsvw' avoids 'ax-13'; $)
   $}
 
   ${
@@ -30778,28 +30790,104 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
 
   $( *** Theorems using axioms up to ax-9 and ax-ext only: *** $)
 
+  ${
+    $d x A $.  $d x B $.
+    $( Equality theorem for restricted existential quantifier.  (Contributed by
+       NM, 29-Oct-1995.)  Remove usage of ~ ax-10 , ~ ax-11 , and ~ ax-12 .
+       (Revised by Steven Nguyen, 30-Apr-2023.)  Shorten other proofs.
+       (Revised by Wolf Lammen, 8-Mar-2025.) $)
+    rexeq $p |- ( A = B -> ( E. x e. A ph <-> E. x e. B ph ) ) $=
+      ( wceq cv wcel wa wex wrex wal dfcleq anbi1 alexbii sylbi df-rex 3bitr4g
+      wb ) CDEZBFZCGZAHZBIZTDGZAHZBIZABCJABDJSUAUDRZBKUCUFRBCDLUGUBUEBUAUDAMNOA
+      BCPABDPQ $.
+
+    $( Equality theorem for restricted universal quantifier.  (Contributed by
+       NM, 16-Nov-1995.)  Remove usage of ~ ax-10 , ~ ax-11 , and ~ ax-12 .
+       (Revised by Steven Nguyen, 30-Apr-2023.)  Shorten other proofs.
+       (Revised by Wolf Lammen, 8-Mar-2025.) $)
+    raleq $p |- ( A = B -> ( A. x e. A ph <-> A. x e. B ph ) ) $=
+      ( wceq wral wn wrex rexeq rexnal 3bitr3g con4bid ) CDEZABCFZABDFZMAGZBCHP
+      BDHNGOGPBCDIABCJABDJKL $.
+  $}
+
+  ${
+    $d A x $.  $d B x $.
+    raleq1i.1 $e |- A = B $.
+    $( Equality inference for restricted universal quantifier.  (Contributed by
+       Paul Chapman, 22-Jun-2011.) $)
+    raleqi $p |- ( A. x e. A ph <-> A. x e. B ph ) $=
+      ( wceq wral wb raleq ax-mp ) CDFABCGABDGHEABCDIJ $.
+
+    $( Equality inference for restricted existential quantifier.  (Contributed
+       by Mario Carneiro, 23-Apr-2015.) $)
+    rexeqi $p |- ( E. x e. A ph <-> E. x e. B ph ) $=
+      ( wceq wrex wb rexeq ax-mp ) CDFABCGABDGHEABCDIJ $.
+  $}
+
+  ${
+    $d x A $.  $d x B $.
+    raleqdv.1 $e |- ( ph -> A = B ) $.
+    $( Equality deduction for restricted universal quantifier.  (Contributed by
+       NM, 13-Nov-2005.) $)
+    raleqdv $p |- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) ) $=
+      ( wceq wral wb raleq syl ) ADEGBCDHBCEHIFBCDEJK $.
+
+    $( Equality deduction for restricted existential quantifier.  (Contributed
+       by NM, 14-Jan-2007.) $)
+    rexeqdv $p |- ( ph -> ( E. x e. A ps <-> E. x e. B ps ) ) $=
+      ( wceq wrex wb rexeq syl ) ADEGBCDHBCEHIFBCDEJK $.
+  $}
+
+  ${
+    $d x A $.  $d x B $.  $d x ph $.
+    raleqbidva.1 $e |- ( ph -> A = B ) $.
+    raleqbidva.2 $e |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) ) $.
+    $( Equality deduction for restricted universal quantifier.  (Contributed by
+       Mario Carneiro, 5-Jan-2017.) $)
+    raleqbidva $p |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) ) $=
+      ( wral ralbidva raleqdv bitrd ) ABDEICDEICDFIABCDEHJACDEFGKL $.
+
+    $( Equality deduction for restricted universal quantifier.  (Contributed by
+       Mario Carneiro, 5-Jan-2017.) $)
+    rexeqbidva $p |- ( ph -> ( E. x e. A ps <-> E. x e. B ch ) ) $=
+      ( wrex rexbidva rexeqdv bitrd ) ABDEICDEICDFIABCDEHJACDEFGKL $.
+  $}
+
   ${
     $d ph x $.  $d A x $.  $d B x $.
     raleqbidvv.1 $e |- ( ph -> A = B ) $.
     raleqbidvv.2 $e |- ( ph -> ( ps <-> ch ) ) $.
     $( Version of ~ raleqbidv with additional disjoint variable conditions, not
        requiring ~ ax-8 nor ~ df-clel .  (Contributed by BJ, 22-Sep-2024.) $)
     raleqbidvv $p |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) ) $=
+      ( wb cv wcel adantr raleqbidva ) ABCDEFGABCIDJEKHLM $.
+    $( $j usage 'raleqbidvv' avoids 'ax-8' 'ax-10' 'ax-11' 'ax-12'
+          'df-clel'; $)
+
+    $( Version of ~ raleqbidv with additional disjoint variable conditions, not
+       requiring ~ ax-8 nor ~ df-clel .  (Contributed by BJ, 22-Sep-2024.)
+       (New usage is discouraged.)  (Proof modification is discouraged.) $)
+    raleqbidvvOLD $p |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) ) $=
       ( cv wcel wi wal wral wb wa alrimiv wceq dfcleq sylib df-ral 19.26 imbi12
       sylanbrc impcom sylg albi syl 3bitr4g ) ADIZEJZBKZDLZUIFJZCKZDLZBDEMCDFMA
       UKUNNZDLULUONABCNZUJUMNZOZUPDAUQDLURDLZUSDLAUQDHPAEFQUTGDEFRSUQURDUAUCURU
       QUPUJUMBCUBUDUEUKUNDUFUGBDETCDFTUH $.
-    $( $j usage 'raleqbidvv' avoids 'ax-8' 'ax-10' 'ax-11' 'ax-12'
-          'df-clel'; $)
 
     $( Version of ~ rexeqbidv with additional disjoint variable conditions, not
        requiring ~ ax-8 nor ~ df-clel .  (Contributed by Wolf Lammen,
        25-Sep-2024.) $)
     rexeqbidvv $p |- ( ph -> ( E. x e. A ps <-> E. x e. B ch ) ) $=
-      ( wrex wn wral notbid raleqbidvv ralnex 3bitr3g con4bid ) ABDEIZCDFIZABJZ
-      DEKCJZDFKQJRJASTDEFGABCHLMBDENCDFNOP $.
+      ( wb cv wcel adantr rexeqbidva ) ABCDEFGABCIDJEKHLM $.
     $( $j usage 'rexeqbidvv' avoids 'ax-8' 'ax-10' 'ax-11' 'ax-12'
           'df-clel'; $)
+
+    $( Version of ~ rexeqbidv with additional disjoint variable conditions, not
+       requiring ~ ax-8 nor ~ df-clel .  (Contributed by Wolf Lammen,
+       25-Sep-2024.)  (New usage is discouraged.)
+       (Proof modification is discouraged.) $)
+    rexeqbidvvOLD $p |- ( ph -> ( E. x e. A ps <-> E. x e. B ch ) ) $=
+      ( wrex wn wral notbid raleqbidvv ralnex 3bitr3g con4bid ) ABDEIZCDFIZABJZ
+      DEKCJZDFKQJRJASTDEFGABCHLMBDENCDFNOP $.
   $}
 
   ${
@@ -30822,45 +30910,19 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
     $d x A $.  $d x B $.
     $( Equality theorem for restricted universal quantifier.  (Contributed by
        NM, 16-Nov-1995.)  Remove usage of ~ ax-10 , ~ ax-11 , and ~ ax-12 .
-       (Revised by Steven Nguyen, 30-Apr-2023.) $)
-    raleq $p |- ( A = B -> ( A. x e. A ph <-> A. x e. B ph ) ) $=
+       (Revised by Steven Nguyen, 30-Apr-2023.)  (New usage is discouraged.)
+       (Proof modification is discouraged.) $)
+    raleqOLD $p |- ( A = B -> ( A. x e. A ph <-> A. x e. B ph ) ) $=
       ( wceq biidd raleqbi1dv ) AABCDCDEAFG $.
 
     $( Equality theorem for restricted existential quantifier.  (Contributed by
        NM, 29-Oct-1995.)  Remove usage of ~ ax-10 , ~ ax-11 , and ~ ax-12 .
-       (Revised by Steven Nguyen, 30-Apr-2023.) $)
-    rexeq $p |- ( A = B -> ( E. x e. A ph <-> E. x e. B ph ) ) $=
+       (Revised by Steven Nguyen, 30-Apr-2023.)  (New usage is discouraged.)
+       (Proof modification is discouraged.) $)
+    rexeqOLD $p |- ( A = B -> ( E. x e. A ph <-> E. x e. B ph ) ) $=
       ( wceq biidd rexeqbi1dv ) AABCDCDEAFG $.
   $}
 
-  ${
-    $d A x $.  $d B x $.
-    raleq1i.1 $e |- A = B $.
-    $( Equality inference for restricted universal quantifier.  (Contributed by
-       Paul Chapman, 22-Jun-2011.) $)
-    raleqi $p |- ( A. x e. A ph <-> A. x e. B ph ) $=
-      ( wceq wral wb raleq ax-mp ) CDFABCGABDGHEABCDIJ $.
-
-    $( Equality inference for restricted existential quantifier.  (Contributed
-       by Mario Carneiro, 23-Apr-2015.) $)
-    rexeqi $p |- ( E. x e. A ph <-> E. x e. B ph ) $=
-      ( wceq wrex wb rexeq ax-mp ) CDFABCGABDGHEABCDIJ $.
-  $}
-
-  ${
-    $d x A $.  $d x B $.
-    raleqdv.1 $e |- ( ph -> A = B ) $.
-    $( Equality deduction for restricted universal quantifier.  (Contributed by
-       NM, 13-Nov-2005.) $)
-    raleqdv $p |- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) ) $=
-      ( wceq wral wb raleq syl ) ADEGBCDHBCEHIFBCDEJK $.
-
-    $( Equality deduction for restricted existential quantifier.  (Contributed
-       by NM, 14-Jan-2007.) $)
-    rexeqdv $p |- ( ph -> ( E. x e. A ps <-> E. x e. B ps ) ) $=
-      ( wceq wrex wb rexeq syl ) ADEGBCDHBCEHIFBCDEJK $.
-  $}
-
   ${
     raleqbii.1 $e |- A = B $.
     raleqbii.2 $e |- ( ps <-> ch ) $.
@@ -30915,21 +30977,6 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
       ( cv wcel eleq2d anbi12d rexbidv2 ) ABCDEFADIZEJNFJBCAEFNGKHLM $.
   $}
 
-  ${
-    $d x A $.  $d x B $.  $d x ph $.
-    raleqbidva.1 $e |- ( ph -> A = B ) $.
-    raleqbidva.2 $e |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) ) $.
-    $( Equality deduction for restricted universal quantifier.  (Contributed by
-       Mario Carneiro, 5-Jan-2017.) $)
-    raleqbidva $p |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) ) $=
-      ( wral ralbidva raleqdv bitrd ) ABDEICDEICDFIABCDEHJACDEFGKL $.
-
-    $( Equality deduction for restricted universal quantifier.  (Contributed by
-       Mario Carneiro, 5-Jan-2017.) $)
-    rexeqbidva $p |- ( ph -> ( E. x e. A ps <-> E. x e. B ch ) ) $=
-      ( wrex rexbidva rexeqdv bitrd ) ABDEICDEICDFIABCDEHJACDEFGKL $.
-  $}
-
   ${
     $d A y $.  $d ps y $.  $d B x $.  $d ch x $.  $d x ph y $.
     cbvraldva2.1 $e |- ( ( ph /\ x = y ) -> ( ps <-> ch ) ) $.