rewrite restricted quantifiers # 7 (#4523)

* move forgotten rsp2e * move ax-10 only theorems * move ax-11 only theorems * discouraged * add missing tag
metamath · Jan 3, 2025 · 5afff8a · 5afff8a
1 parent 4edddb3
commit 5afff8a
Show file tree

Hide file tree

Showing 2 changed files with 151 additions and 144 deletions.
diff --git a/discouraged b/discouraged
@@ -18731,6 +18731,7 @@ New usage of "rabrabiOLD" is discouraged (0 uses).
 New usage of "ral0OLD" is discouraged (0 uses).
 New usage of "ralabOLD" is discouraged (0 uses).
 New usage of "ralbidaOLD" is discouraged (0 uses).
+New usage of "ralcom13OLD" is discouraged (0 uses).
 New usage of "ralcom2" is discouraged (0 uses).
 New usage of "ralcom3OLD" is discouraged (0 uses).
 New usage of "ralcom4OLD" is discouraged (0 uses).
@@ -21115,6 +21116,7 @@ Proof modification of "rabrabiOLD" is discouraged (38 steps).
 Proof modification of "ral0OLD" is discouraged (12 steps).
 Proof modification of "ralabOLD" is discouraged (40 steps).
 Proof modification of "ralbidaOLD" is discouraged (43 steps).
+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).

diff --git a/set.mm b/set.mm
@@ -30008,6 +30008,12 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
   rsp2 $p |- ( A. x e. A A. y e. B ph -> ( ( x e. A /\ y e. B ) -> ph ) ) $=
     ( wral cv wcel wi rsp syl6 impd ) ACEFZBDFZBGDHZCGEHZANOMPAIMBDJACEJKL $.
 
+  $( Restricted specialization.  (Contributed by FL, 4-Jun-2012.)  (Proof
+     shortened by Wolf Lammen, 7-Jan-2020.) $)
+  rsp2e $p |- ( ( x e. A /\ y e. B /\ ph ) -> E. x e. A E. y e. B ph ) $=
+    ( cv wcel wrex wa rspe sylan2 3impb ) BFDGZCFEGZAACEHZBDHZNAIMOPACEJOBDJKL
+    $.
+
   ${
     rspec2.1 $e |- A. x e. A A. y e. B ph $.
     $( Specialization rule for restricted quantification, with two quantifiers.
@@ -30060,6 +30066,149 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
       EITEOPATELGMBCQJRSS $.
   $}
 
+  $( *** Theorems using axioms up to ax-8 and ax-10 only: *** $)
+
+  $( The setvar ` x ` is not free in ` A. x e. A ph ` .  (Contributed by NM,
+     18-Oct-1996.)  (Revised by Mario Carneiro, 7-Oct-2016.) $)
+  nfra1 $p |- F/ x A. x e. A ph $=
+    ( wral cv wcel wi wal df-ral nfa1 nfxfr ) ABCDBECFAGZBHBABCILBJK $.
+
+  $( The setvar ` x ` is not free in ` E. x e. A ph ` .  (Contributed by NM,
+     19-Mar-1997.)  (Revised by Mario Carneiro, 7-Oct-2016.) $)
+  nfre1 $p |- F/ x E. x e. A ph $=
+    ( wrex cv wcel wa wex df-rex nfe1 nfxfr ) ABCDBECFAGZBHBABCILBJK $.
+
+  $( *** Theorems using axioms up to ax-8 and ax-11 only: *** $)
+
+  ${
+    $d x y $.  $d y A $.
+    $( Commutation of restricted and unrestricted universal quantifiers.
+       (Contributed by NM, 26-Mar-2004.)  (Proof shortened by Andrew Salmon,
+       8-Jun-2011.)  Reduce axiom dependencies.  (Revised by BJ, 13-Jun-2019.)
+       (Proof shortened by Wolf Lammen, 31-Oct-2024.) $)
+    ralcom4 $p |- ( A. x e. A A. y ph <-> A. y A. x e. A ph ) $=
+      ( wal wral cv wcel wi 19.21v albii alcom df-ral 3bitr4ri bitr4i ) ACEZBDF
+      ZBGDHZAIZBEZCEZABDFZCESCEZBERPIZBEUAQUCUDBRACJKSCBLPBDMNUBTCABDMKO $.
+
+    $( Obsolete version of ~ ralcom4 as of 31-Oct-2024.  (Contributed by NM,
+       26-Mar-2004.)  (Proof shortened by Andrew Salmon, 8-Jun-2011.)  Reduce
+       axiom dependencies.  (Revised by BJ, 13-Jun-2019.)
+       (New usage is discouraged.)  (Proof modification is discouraged.) $)
+    ralcom4OLD $p |- ( A. x e. A A. y ph <-> A. y A. x e. A ph ) $=
+      ( cv wcel wal wi wral 19.21v bicomi albii alcom bitri df-ral 3bitr4i ) BE
+      DFZACGZHZBGZQAHZBGZCGZRBDIABDIZCGTUACGZBGUCSUEBUESQACJKLUABCMNRBDOUDUBCAB
+      DOLP $.
+
+    $( Commutation of restricted and unrestricted existential quantifiers.
+       (Contributed by NM, 12-Apr-2004.)  (Proof shortened by Andrew Salmon,
+       8-Jun-2011.)  Reduce axiom dependencies.  (Revised by BJ,
+       13-Jun-2019.) $)
+    rexcom4 $p |- ( E. x e. A E. y ph <-> E. y E. x e. A ph ) $=
+      ( cv wcel wa wex wrex exdistr df-rex exbii excom bitri 3bitr4ri ) BEDFZAG
+      ZCHBHZPACHZGBHABDIZCHZSBDIPABCJUAQBHZCHRTUBCABDKLQCBMNSBDKO $.
+
+    $d x B $.
+    $( Commutation of restricted universal quantifiers.  See ~ ralcom2 for a
+       version without disjoint variable condition on ` x , y ` .  This theorem
+       should be used in place of ~ ralcom2 since it depends on a smaller set
+       of axioms.  (Contributed by NM, 13-Oct-1999.)  (Revised by Mario
+       Carneiro, 14-Oct-2016.) $)
+    ralcom $p |- ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph ) $=
+      ( cv wcel wa wi wal wral ancomst 2albii alcom bitri r2al 3bitr4i ) BFDGZC
+      FEGZHAIZCJBJZSRHAIZBJCJZACEKBDKABDKCEKUAUBCJBJUCTUBBCRSALMUBBCNOABCDEPACB
+      EDPQ $.
+    $( $j usage 'ralcom' avoids 'ax-6' 'ax-7' 'ax-8' 'ax-9' 'ax-10' 'ax-12'
+       'ax-13' 'ax-ext'; $)
+
+    $( Commutation of restricted existential quantifiers.  (Contributed by NM,
+       19-Nov-1995.)  (Revised by Mario Carneiro, 14-Oct-2016.)  (Proof
+       shortened by BJ, 26-Aug-2023.)  (Proof shortened by Wolf Lammen,
+       8-Dec-2024.) $)
+    rexcom $p |- ( E. x e. A E. y e. B ph <-> E. y e. B E. x e. A ph ) $=
+      ( wrex wn wral ralcom ralnex2 3bitr3i con4bii ) ACEFBDFZABDFCEFZAGZCEHBDH
+      OBDHCEHMGNGOBCDEIABCDEJACBEDJKL $.
+    $( $j usage 'rexcom' avoids 'ax-6' 'ax-7' 'ax-8' 'ax-9' 'ax-10' 'ax-12'
+       'ax-13' 'ax-ext'; $)
+
+    $( Obsolete version of ~ rexcom as of 8-Dec-2024.  (Contributed by NM,
+       19-Nov-1995.)  (Revised by Mario Carneiro, 14-Oct-2016.)  (Proof
+       shortened by BJ, 26-Aug-2023.)  (New usage is discouraged.)
+       (Proof modification is discouraged.) $)
+    rexcomOLD $p |- ( E. x e. A E. y e. B ph <-> E. y e. B E. x e. A ph ) $=
+      ( wrex cv wcel wa wex df-rex rexbii rexcom4 r19.42v exbii bitr4i 3bitri )
+      ACEFZBDFCGEHZAIZCJZBDFTBDFZCJZABDFZCEFZRUABDACEKLTBCDMUCSUDIZCJUEUBUFCSAB
+      DNOUDCEKPQ $.
+    $( $j usage 'rexcomOLD' avoids 'ax-6' 'ax-7' 'ax-8' 'ax-9' 'ax-10' 'ax-12'
+       'ax-13' 'ax-ext'; $)
+  $}
+
+  ${
+    $d x A $.  $d x y $.  $d x ph $.
+    $( Specialized existential commutation lemma.  (Contributed by Jeff Madsen,
+       1-Jun-2011.) $)
+    rexcom4a $p |- ( E. x E. y e. A ( ph /\ ps ) <->
+                                               E. y e. A ( ph /\ E. x ps ) ) $=
+      ( wa wrex wex rexcom4 19.42v rexbii bitr3i ) ABFZDEGCHMCHZDEGABCHFZDEGMDC
+      EINODEABCJKL $.
+  $}
+
+  ${
+    $d z A $.  $d z B $.  $d x C $.  $d y C $.  $d x z $.  $d y z $.
+    $( Rotate three restricted universal quantifiers.  (Contributed by AV,
+       3-Dec-2021.) $)
+    ralrot3 $p |- ( A. x e. A A. y e. B A. z e. C ph
+                    <-> A. z e. C A. x e. A A. y e. B ph ) $=
+      ( wral ralcom ralbii bitri ) ADGHCFHZBEHACFHZDGHZBEHMBEHDGHLNBEACDFGIJMBD
+      EGIK $.
+  $}
+
+  ${
+    $d y z A $.  $d x z B $.  $d x y C $.
+    $( Swap first and third restricted universal quantifiers.  (Contributed by
+       AV, 3-Dec-2021.)  (Proof shortened by Wolf Lammen, 2-Jan-2025.) $)
+    ralcom13 $p |- ( A. x e. A A. y e. B A. z e. C ph
+         <-> A. z e. C A. y e. B A. x e. A ph ) $=
+      ( wral ralrot3 ralcom ralbii bitri ) ADGHCFHBEHACFHBEHZDGHABEHCFHZDGHABCD
+      EFGIMNDGABCEFJKL $.
+
+    $( Obsolete version of ~ ralcom13 as of 2-Jan-2025.  (Contributed by AV,
+       3-Dec-2021.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    ralcom13OLD $p |- ( A. x e. A A. y e. B A. z e. C ph
+         <-> A. z e. C A. y e. B A. x e. A ph ) $=
+      ( wral ralcom ralbii 3bitri ) ADGHZCFHBEHLBEHZCFHABEHZDGHZCFHNCFHDGHLBCEF
+      IMOCFABDEGIJNCDFGIK $.
+
+    $( Swap first and third restricted existential quantifiers.  (Contributed
+       by NM, 8-Apr-2015.) $)
+    rexcom13 $p |- ( E. x e. A E. y e. B E. z e. C ph
+         <-> E. z e. C E. y e. B E. x e. A ph ) $=
+      ( wrex rexcom rexbii 3bitri ) ADGHZCFHBEHLBEHZCFHABEHZDGHZCFHNCFHDGHLBCEF
+      IMOCFABDEGIJNCDFGIK $.
+  $}
+
+  ${
+    $d w z A $.  $d w z B $.  $d w x C $.  $d w y C $.  $d x z D $.
+    $d y z D $.
+    $( Rotate four restricted existential quantifiers twice.  (Contributed by
+       NM, 8-Apr-2015.) $)
+    rexrot4 $p |- ( E. x e. A E. y e. B E. z e. C E. w e. D ph
+        <-> E. z e. C E. w e. D E. x e. A E. y e. B ph ) $=
+      ( wrex rexcom13 rexbii bitri ) AEIJDHJCGJZBFJACGJZDHJEIJZBFJOBFJEIJDHJNPB
+      FACDEGHIKLOBEDFIHKM $.
+  $}
+
+  ${
+    $d A x $.  $d A y $.  $d B x $.  $d B y $.  $d w x $.  $d w y $.  $d x z $.
+    $d y z $.
+    $( Rotate two existential quantifiers and two restricted existential
+       quantifiers.  (Contributed by AV, 9-Nov-2023.) $)
+    2ex2rexrot $p |- ( E. x E. y E. z e. A E. w e. B ph
+                       <-> E. z e. A E. w e. B E. x E. y ph ) $=
+      ( wex wrex rexcom4 rexbii bitri exbii 3bitrri ) ACHZBHEGIZDFIOEGIZBHZDFIQ
+      DFIZBHAEGIZDFICHZBHPRDFOEBGJKQDBFJSUABSTCHZDFIUAQUBDFAECGJKTDCFJLMN $.
+  $}
+
   $( Extend wff notation to include restricted existential uniqueness. $)
   wreu $a wff E! x e. A ph $.
 
@@ -30108,11 +30257,6 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
      ~ df-ral .  (Contributed by NM, 22-Nov-1994.) $)
   df-rab $a |- { x e. A | ph } = { x | ( x e. A /\ ph ) } $.
 
-  $( The setvar ` x ` is not free in ` A. x e. A ph ` .  (Contributed by NM,
-     18-Oct-1996.)  (Revised by Mario Carneiro, 7-Oct-2016.) $)
-  nfra1 $p |- F/ x A. x e. A ph $=
-    ( wral cv wcel wi wal df-ral nfa1 nfxfr ) ABCDBECFAGZBHBABCILBJK $.
-
   $( The setvar ` x ` is not free in ` A. x e. A ph ` .  (Contributed by NM,
      18-Oct-1996.)  (Proof shortened by Wolf Lammen, 7-Dec-2019.) $)
   hbra1 $p |- ( A. x e. A ph -> A. x A. x e. A ph ) $=
@@ -30267,93 +30411,6 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
       ( cv wcel eleq2i imbi12i ralbii2 ) ABCDECHZDIMEIABDEMFJGKL $.
   $}
 
-  ${
-    $d x y $.  $d y A $.
-    $( Commutation of restricted and unrestricted universal quantifiers.
-       (Contributed by NM, 26-Mar-2004.)  (Proof shortened by Andrew Salmon,
-       8-Jun-2011.)  Reduce axiom dependencies.  (Revised by BJ, 13-Jun-2019.)
-       (Proof shortened by Wolf Lammen, 31-Oct-2024.) $)
-    ralcom4 $p |- ( A. x e. A A. y ph <-> A. y A. x e. A ph ) $=
-      ( wal wral cv wcel wi 19.21v albii alcom df-ral 3bitr4ri bitr4i ) ACEZBDF
-      ZBGDHZAIZBEZCEZABDFZCESCEZBERPIZBEUAQUCUDBRACJKSCBLPBDMNUBTCABDMKO $.
-
-    $( Obsolete version of ~ ralcom4 as of 31-Oct-2024.  (Contributed by NM,
-       26-Mar-2004.)  (Proof shortened by Andrew Salmon, 8-Jun-2011.)  Reduce
-       axiom dependencies.  (Revised by BJ, 13-Jun-2019.)
-       (New usage is discouraged.)  (Proof modification is discouraged.) $)
-    ralcom4OLD $p |- ( A. x e. A A. y ph <-> A. y A. x e. A ph ) $=
-      ( cv wcel wal wi wral 19.21v bicomi albii alcom bitri df-ral 3bitr4i ) BE
-      DFZACGZHZBGZQAHZBGZCGZRBDIABDIZCGTUACGZBGUCSUEBUESQACJKLUABCMNRBDOUDUBCAB
-      DOLP $.
-
-    $d x B $.
-    $( Commutation of restricted universal quantifiers.  See ~ ralcom2 for a
-       version without disjoint variable condition on ` x , y ` .  This theorem
-       should be used in place of ~ ralcom2 since it depends on a smaller set
-       of axioms.  (Contributed by NM, 13-Oct-1999.)  (Revised by Mario
-       Carneiro, 14-Oct-2016.) $)
-    ralcom $p |- ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph ) $=
-      ( cv wcel wa wi wal wral ancomst 2albii alcom bitri r2al 3bitr4i ) BFDGZC
-      FEGZHAIZCJBJZSRHAIZBJCJZACEKBDKABDKCEKUAUBCJBJUCTUBBCRSALMUBBCNOABCDEPACB
-      EDPQ $.
-    $( $j usage 'ralcom' avoids 'ax-6' 'ax-7' 'ax-8' 'ax-9' 'ax-10' 'ax-12'
-       'ax-13' 'ax-ext'; $)
-  $}
-
-  ${
-    $d x y $.  $d y A $.
-    $( Commutation of restricted and unrestricted existential quantifiers.
-       (Contributed by NM, 12-Apr-2004.)  (Proof shortened by Andrew Salmon,
-       8-Jun-2011.)  Reduce axiom dependencies.  (Revised by BJ,
-       13-Jun-2019.) $)
-    rexcom4 $p |- ( E. x e. A E. y ph <-> E. y E. x e. A ph ) $=
-      ( cv wcel wa wex wrex exdistr df-rex exbii excom bitri 3bitr4ri ) BEDFZAG
-      ZCHBHZPACHZGBHABDIZCHZSBDIPABCJUAQBHZCHRTUBCABDKLQCBMNSBDKO $.
-
-    $d x B $.
-    $( Commutation of restricted existential quantifiers.  (Contributed by NM,
-       19-Nov-1995.)  (Revised by Mario Carneiro, 14-Oct-2016.)  (Proof
-       shortened by BJ, 26-Aug-2023.)  (Proof shortened by Wolf Lammen,
-       8-Dec-2024.) $)
-    rexcom $p |- ( E. x e. A E. y e. B ph <-> E. y e. B E. x e. A ph ) $=
-      ( wrex wn wral ralcom ralnex2 3bitr3i con4bii ) ACEFBDFZABDFCEFZAGZCEHBDH
-      OBDHCEHMGNGOBCDEIABCDEJACBEDJKL $.
-    $( $j usage 'rexcom' avoids 'ax-6' 'ax-7' 'ax-8' 'ax-9' 'ax-10' 'ax-12'
-       'ax-13' 'ax-ext'; $)
-  $}
-
-  ${
-    $d A x $.  $d A y $.  $d B x $.  $d B y $.  $d w x $.  $d w y $.  $d x z $.
-    $d y z $.
-    $( Rotate two existential quantifiers and two restricted existential
-       quantifiers.  (Contributed by AV, 9-Nov-2023.) $)
-    2ex2rexrot $p |- ( E. x E. y E. z e. A E. w e. B ph
-                       <-> E. z e. A E. w e. B E. x E. y ph ) $=
-      ( wex wrex rexcom4 rexbii bitri exbii 3bitrri ) ACHZBHEGIZDFIOEGIZBHZDFIQ
-      DFIZBHAEGIZDFICHZBHPRDFOEBGJKQDBFJSUABSTCHZDFIUAQUBDFAECGJKTDCFJLMN $.
-  $}
-
-  ${
-    $d x A $.  $d x y $.  $d x ph $.
-    $( Specialized existential commutation lemma.  (Contributed by Jeff Madsen,
-       1-Jun-2011.) $)
-    rexcom4a $p |- ( E. x E. y e. A ( ph /\ ps ) <->
-                                               E. y e. A ( ph /\ E. x ps ) ) $=
-      ( wa wrex wex rexcom4 19.42v rexbii bitr3i ) ABFZDEGCHMCHZDEGABCHFZDEGMDC
-      EINODEABCJKL $.
-  $}
-
-  $( Restricted specialization.  (Contributed by FL, 4-Jun-2012.)  (Proof
-     shortened by Wolf Lammen, 7-Jan-2020.) $)
-  rsp2e $p |- ( ( x e. A /\ y e. B /\ ph ) -> E. x e. A E. y e. B ph ) $=
-    ( cv wcel wrex wa rspe sylan2 3impb ) BFDGZCFEGZAACEHZBDHZNAIMOPACEJOBDJKL
-    $.
-
-  $( The setvar ` x ` is not free in ` E. x e. A ph ` .  (Contributed by NM,
-     19-Mar-1997.)  (Revised by Mario Carneiro, 7-Oct-2016.) $)
-  nfre1 $p |- F/ x E. x e. A ph $=
-    ( wrex cv wcel wa wex df-rex nfe1 nfxfr ) ABCDBECFAGZBHBABCILBJK $.
-
   ${
     $d x y $.
     nfrexd.1 $e |- F/ y ph $.
@@ -30464,58 +30521,6 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
       BCPQABCDEFRACBEDGRS $.
   $}
 
-  ${
-    $d x y $.  $d y A $.  $d x B $.
-    $( Obsolete version of ~ rexcom as of 8-Dec-2024.  (Contributed by NM,
-       19-Nov-1995.)  (Revised by Mario Carneiro, 14-Oct-2016.)  (Proof
-       shortened by BJ, 26-Aug-2023.)  (New usage is discouraged.)
-       (Proof modification is discouraged.) $)
-    rexcomOLD $p |- ( E. x e. A E. y e. B ph <-> E. y e. B E. x e. A ph ) $=
-      ( wrex cv wcel wa wex df-rex rexbii rexcom4 r19.42v exbii bitr4i 3bitri )
-      ACEFZBDFCGEHZAIZCJZBDFTBDFZCJZABDFZCEFZRUABDACEKLTBCDMUCSUDIZCJUEUBUFCSAB
-      DNOUDCEKPQ $.
-    $( $j usage 'rexcomOLD' avoids 'ax-6' 'ax-7' 'ax-8' 'ax-9' 'ax-10' 'ax-12'
-       'ax-13' 'ax-ext'; $)
-  $}
-
-  ${
-    $d y z A $.  $d x z B $.  $d x y C $.
-    $( Swap first and third restricted universal quantifiers.  (Contributed by
-       AV, 3-Dec-2021.) $)
-    ralcom13 $p |- ( A. x e. A A. y e. B A. z e. C ph
-         <-> A. z e. C A. y e. B A. x e. A ph ) $=
-      ( wral ralcom ralbii 3bitri ) ADGHZCFHBEHLBEHZCFHABEHZDGHZCFHNCFHDGHLBCEF
-      IMOCFABDEGIJNCDFGIK $.
-
-    $( Swap first and third restricted existential quantifiers.  (Contributed
-       by NM, 8-Apr-2015.) $)
-    rexcom13 $p |- ( E. x e. A E. y e. B E. z e. C ph
-         <-> E. z e. C E. y e. B E. x e. A ph ) $=
-      ( wrex rexcom rexbii 3bitri ) ADGHZCFHBEHLBEHZCFHABEHZDGHZCFHNCFHDGHLBCEF
-      IMOCFABDEGIJNCDFGIK $.
-  $}
-
-  ${
-    $d z A $.  $d z B $.  $d x C $.  $d y C $.  $d x z $.  $d y z $.
-    $( Rotate three restricted universal quantifiers.  (Contributed by AV,
-       3-Dec-2021.) $)
-    ralrot3 $p |- ( A. x e. A A. y e. B A. z e. C ph
-                    <-> A. z e. C A. x e. A A. y e. B ph ) $=
-      ( wral ralcom ralbii bitri ) ADGHCFHZBEHACFHZDGHZBEHMBEHDGHLNBEACDFGIJMBD
-      EGIK $.
-  $}
-
-  ${
-    $d w z A $.  $d w z B $.  $d w x C $.  $d w y C $.  $d x z D $.
-    $d y z D $.
-    $( Rotate four restricted existential quantifiers twice.  (Contributed by
-       NM, 8-Apr-2015.) $)
-    rexrot4 $p |- ( E. x e. A E. y e. B E. z e. C E. w e. D ph
-        <-> E. z e. C E. w e. D E. x e. A E. y e. B ph ) $=
-      ( wrex rexcom13 rexbii bitri ) AEIJDHJCGJZBFJACGJZDHJEIJZBFJOBFJEIJDHJNPB
-      FACDEGHIKLOBEDFIHKM $.
-  $}
-
   ${
     $d y A $.  $d x A $.
     $( Commutation of restricted universal quantifiers.  Note that ` x ` and