rewrite restricted quantifiers # 12 (metamath#4552)

* rewrite rmo/reu, up to ax-5 * move forgotten cbvralf
mazsa · Jan 11, 2025 · fd2693e · fd2693e
1 parent e37738a
commit fd2693e
Showing 1 changed file with 135 additions and 141 deletions.
diff --git a/set.mm b/set.mm
@@ -30923,16 +30923,39 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
       $.
   $}
 
+  ${
+    $d x z $.  $d y z $.  $d z A $.  $d z ps $.  $d z ph $.
+    cbvralf.1 $e |- F/_ x A $.
+    cbvralf.2 $e |- F/_ y A $.
+    cbvralf.3 $e |- F/ y ph $.
+    cbvralf.4 $e |- F/ x ps $.
+    cbvralf.5 $e |- ( x = y -> ( ph <-> ps ) ) $.
+    $( Rule used to change bound variables, using implicit substitution.  Usage
+       of this theorem is discouraged because it depends on ~ ax-13 .  Use the
+       weaker ~ cbvralfw when possible.  (Contributed by NM, 7-Mar-2004.)
+       (Revised by Mario Carneiro, 9-Oct-2016.)  (New usage is discouraged.) $)
+    cbvralf $p |- ( A. x e. A ph <-> A. y e. A ps ) $=
+      ( vz cv wcel wi wal wral wsb nfv nfcri nfim nfs1v sbequ12 imbi12d cbvalv1
+      weq eleq1w nfsb sbequ sbie bitrdi bitri df-ral 3bitr4i ) CLEMZANZCOZDLEMZ
+      BNZDOZACEPBDEPUPKLEMZACKQZNZKOUSUOVBCKUOKRUTVACCKEFSACKUATCKUEUNUTAVACKEU
+      FACKUBUCUDVBURKDUTVADDKEGSACKDHUGTURKRKDUEZUTUQVABKDEUFVCVAACDQBAKDCUHABC
+      DIJUIUJUCUDUKACEULBDEULUM $.
+
+    $( Rule used to change bound variables, using implicit substitution.  Usage
+       of this theorem is discouraged because it depends on ~ ax-13 .  Use the
+       weaker ~ cbvrexfw when possible.  (Contributed by FL, 27-Apr-2008.)
+       (Revised by Mario Carneiro, 9-Oct-2016.)  (New usage is discouraged.) $)
+    cbvrexf $p |- ( E. x e. A ph <-> E. y e. A ps ) $=
+      ( wn wral wrex nfn weq notbid cbvralf notbii dfrex2 3bitr4i ) AKZCELZKBKZ
+      DELZKACEMBDEMUBUDUAUCCDEFGADHNBCINCDOABJPQRACESBDEST $.
+  $}
+
   $( Extend wff notation to include restricted existential uniqueness. $)
   wreu $a wff E! x e. A ph $.
 
   $( Extend wff notation to include restricted "at most one". $)
   wrmo $a wff E* x e. A ph $.
 
-  $( Extend class notation to include the restricted class abstraction (class
-     builder). $)
-  crab $a class { x e. A | ph } $.
-
   $( Define restricted "at most one".
 
      Note:  This notation is most often used to express that ` ph ` holds for
@@ -30959,6 +30982,113 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
      (Contributed by NM, 22-Nov-1994.) $)
   df-reu $a |- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) ) $.
 
+  $( *** Theorems using axioms up to ax-4 only: *** $)
+
+  $( Restricted uniqueness in terms of "at most one".  (Contributed by NM,
+     23-May-1999.)  (Revised by NM, 16-Jun-2017.) $)
+  reu5 $p |- ( E! x e. A ph <-> ( E. x e. A ph /\ E* x e. A ph ) ) $=
+    ( cv wcel wa weu wex wmo wreu wrex wrmo df-eu df-reu df-rex anbi12i 3bitr4i
+    df-rmo ) BDCEAFZBGSBHZSBIZFABCJABCKZABCLZFSBMABCNUBTUCUAABCOABCRPQ $.
+
+  $( Restricted existential uniqueness implies restricted "at most one."
+     (Contributed by NM, 16-Jun-2017.) $)
+  reurmo $p |- ( E! x e. A ph -> E* x e. A ph ) $=
+    ( wreu wrex wrmo reu5 simprbi ) ABCDABCEABCFABCGH $.
+
+  $( Restricted unique existence implies restricted existence.  (Contributed by
+     NM, 19-Aug-1999.) $)
+  reurex $p |- ( E! x e. A ph -> E. x e. A ph ) $=
+    ( wreu wrex wrmo reu5 simplbi ) ABCDABCEABCFABCGH $.
+
+  $( Unrestricted "at most one" implies restricted "at most one".  (Contributed
+     by NM, 16-Jun-2017.) $)
+  mormo $p |- ( E* x ph -> E* x e. A ph ) $=
+    ( wmo cv wcel wa wrmo moan df-rmo sylibr ) ABDBECFZAGBDABCHALBIABCJK $.
+
+  $( Cancellation law for restricted at-most-one quantification.  (Contributed
+     by Peter Mazsa, 24-May-2018.) $)
+  rmoanid $p |- ( E* x e. A ( x e. A /\ ph ) <-> E* x e. A ph ) $=
+    ( cv wcel wa wmo wrmo anabs5 mobii df-rmo 3bitr4i ) BDCEZMAFZFZBGNBGNBCHABC
+    HONBMAIJNBCKABCKL $.
+
+  $( Cancellation law for restricted unique existential quantification.
+     (Contributed by Peter Mazsa, 12-Feb-2018.) $)
+  reuanid $p |- ( E! x e. A ( x e. A /\ ph ) <-> E! x e. A ph ) $=
+    ( cv wcel wa weu wreu anabs5 eubii df-reu 3bitr4i ) BDCEZMAFZFZBGNBGNBCHABC
+    HONBMAIJNBCKABCKL $.
+
+  ${
+    rmobiia.1 $e |- ( x e. A -> ( ph <-> ps ) ) $.
+    $( Formula-building rule for restricted existential 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.) $)
+    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 $.
+  $}
+
+  ${
+    rmobii.1 $e |- ( ph <-> ps ) $.
+    $( Formula-building rule for restricted existential 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.) $)
+    reubii $p |- ( E! x e. A ph <-> E! x e. A ps ) $=
+      ( wb cv wcel a1i reubiia ) ABCDABFCGDHEIJ $.
+  $}
+
+  $( Double restricted existential uniqueness, analogous to ~ 2eu2ex .
+     (Contributed by Alexander van der Vekens, 25-Jun-2017.) $)
+  2reu2rex $p |- ( E! x e. A E! y e. B ph -> E. x e. A E. y e. B ph ) $=
+    ( wreu wrex reurex reximi syl ) ACEFZBDFKBDGACEGZBDGKBDHKLBDACEHIJ $.
+
+  $( *** Theorems using axioms up to ax-5 only: *** $)
+
+  ${
+    $d x ph $.
+    rmobidva.1 $e |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) ) $.
+    $( Formula-building rule for restricted existential 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 ) ) $=
+      ( cv wcel wa wmo wrmo pm5.32da mobidv df-rmo 3bitr4g ) ADGEHZBIZDJPCIZDJB
+      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.) $)
+    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 $.
+  $}
+
+  ${
+    $d x ph $.
+    rmobidv.1 $e |- ( ph -> ( ps <-> ch ) ) $.
+    $( Formula-building rule for restricted existential 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.) $)
+    reubidv $p |- ( ph -> ( E! x e. A ps <-> E! x e. A ch ) ) $=
+      ( wb cv wcel adantr reubidva ) ABCDEABCGDHEIFJK $.
+  $}
+
+  $( Extend class notation to include the restricted class abstraction (class
+     builder). $)
+  crab $a class { x e. A | ph } $.
+
   $( Define a restricted class abstraction (class builder): ` { x e. A | ph } `
      is the class of all sets ` x ` in ` A ` such that ` ph ( x ) ` is true.
      Definition of [TakeutiZaring] p. 20.
@@ -30971,18 +31101,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 ) } $.
 
-  $( Cancellation law for restricted unique existential quantification.
-     (Contributed by Peter Mazsa, 12-Feb-2018.) $)
-  reuanid $p |- ( E! x e. A ( x e. A /\ ph ) <-> E! x e. A ph ) $=
-    ( cv wcel wa weu wreu anabs5 eubii df-reu 3bitr4i ) BDCEZMAFZFZBGNBGNBCHABC
-    HONBMAIJNBCKABCKL $.
-
-  $( Cancellation law for restricted at-most-one quantification.  (Contributed
-     by Peter Mazsa, 24-May-2018.) $)
-  rmoanid $p |- ( E* x e. A ( x e. A /\ ph ) <-> E* x e. A ph ) $=
-    ( cv wcel wa wmo wrmo anabs5 mobii df-rmo 3bitr4i ) BDCEZMAFZFZBGNBGNBCHABC
-    HONBMAIJNBCKABCKL $.
-
   $( The setvar ` x ` is not free in ` E! x e. A ph ` .  (Contributed by NM,
      19-Mar-1997.) $)
   nfreu1 $p |- F/ x E! x e. A ph $=
@@ -31185,43 +31303,6 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
       ELCDELARSDFAQBCGMNBDEOCDEOP $.
   $}
 
-  ${
-    $d x ph $.
-    reubidva.1 $e |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) ) $.
-    $( 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.) $)
-    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 $.
-  $}
-
-  ${
-    $d x ph $.
-    reubidv.1 $e |- ( ph -> ( ps <-> ch ) ) $.
-    $( Formula-building rule for restricted existential 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 $.
-  $}
-
-  ${
-    reubiia.1 $e |- ( x e. A -> ( ph <-> ps ) ) $.
-    $( Formula-building rule for restricted existential 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 $.
-  $}
-
-  ${
-    reubii.1 $e |- ( ph <-> ps ) $.
-    $( Formula-building rule for restricted existential 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 $.
-  $}
-
   ${
     rmobida.1 $e |- F/ x ph $.
     rmobida.2 $e |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) ) $.
@@ -31234,48 +31315,14 @@ 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
-       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 ) ) $=
-      ( cv wcel wa wmo wrmo pm5.32da mobidv df-rmo 3bitr4g ) ADGEHZBIZDJPCIZDJB
-      DEKCDEKAQRDAPBCFLMBDENCDENO $.
-    $( $j usage 'rmobidva' avoids 'ax-6' 'ax-7' 'ax-12'; $)
-
+    rmobidvaOLD.1 $e |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) ) $.
     $( Obsolete version of ~ rmobidv as of 23-Nov-2024.  (Contributed by NM,
        16-Jun-2017.)  (Proof modification is discouraged.)
        (New usage is discouraged.) $)
     rmobidvaOLD $p |- ( ph -> ( E* x e. A ps <-> E* x e. A ch ) ) $=
       ( nfv rmobida ) ABCDEADGFH $.
   $}
 
-  ${
-    $d x ph $.
-    rmobidv.1 $e |- ( ph -> ( ps <-> ch ) ) $.
-    $( Formula-building rule for restricted existential 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 $.
-  $}
-
-  ${
-    rmobiia.1 $e |- ( x e. A -> ( ph <-> ps ) ) $.
-    $( Formula-building rule for restricted existential 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 $.
-  $}
-
-  ${
-    rmobii.1 $e |- ( ph <-> ps ) $.
-    $( Formula-building rule for restricted existential 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 $.
-  $}
-
   ${
     reueq1f.1 $e |- F/_ x A $.
     reueq1f.2 $e |- F/_ x B $.
@@ -31347,32 +31394,6 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
       JUEGZAHUMUEACKULUNAUJUCUDQSTSUAUB $.
   $}
 
-  $( Unrestricted "at most one" implies restricted "at most one".  (Contributed
-     by NM, 16-Jun-2017.) $)
-  mormo $p |- ( E* x ph -> E* x e. A ph ) $=
-    ( wmo cv wcel wa wrmo moan df-rmo sylibr ) ABDBECFZAGBDABCHALBIABCJK $.
-
-  $( Restricted uniqueness in terms of "at most one".  (Contributed by NM,
-     23-May-1999.)  (Revised by NM, 16-Jun-2017.) $)
-  reu5 $p |- ( E! x e. A ph <-> ( E. x e. A ph /\ E* x e. A ph ) ) $=
-    ( cv wcel wa weu wex wmo wreu wrex wrmo df-eu df-reu df-rex anbi12i 3bitr4i
-    df-rmo ) BDCEAFZBGSBHZSBIZFABCJABCKZABCLZFSBMABCNUBTUCUAABCOABCRPQ $.
-
-  $( Restricted unique existence implies restricted existence.  (Contributed by
-     NM, 19-Aug-1999.) $)
-  reurex $p |- ( E! x e. A ph -> E. x e. A ph ) $=
-    ( wreu wrex wrmo reu5 simplbi ) ABCDABCEABCFABCGH $.
-
-  $( Double restricted existential uniqueness, analogous to ~ 2eu2ex .
-     (Contributed by Alexander van der Vekens, 25-Jun-2017.) $)
-  2reu2rex $p |- ( E! x e. A E! y e. B ph -> E. x e. A E. y e. B ph ) $=
-    ( wreu wrex reurex reximi syl ) ACEFZBDFKBDGACEGZBDGKBDHKLBDACEHIJ $.
-
-  $( Restricted existential uniqueness implies restricted "at most one."
-     (Contributed by NM, 16-Jun-2017.) $)
-  reurmo $p |- ( E! x e. A ph -> E* x e. A ph ) $=
-    ( wreu wrex wrmo reu5 simprbi ) ABCDABCEABCFABCGH $.
-
   $( Restricted "at most one" in term of uniqueness.  (Contributed by NM,
      16-Jun-2017.) $)
   rmo5 $p |- ( E* x e. A ph <-> ( E. x e. A ph -> E! x e. A ph ) ) $=
@@ -31395,33 +31416,6 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
       BCJBCDKABQCABPABPELMNO $.
   $}
 
-  ${
-    $d x z $.  $d y z $.  $d z A $.  $d z ps $.  $d z ph $.
-    cbvralf.1 $e |- F/_ x A $.
-    cbvralf.2 $e |- F/_ y A $.
-    cbvralf.3 $e |- F/ y ph $.
-    cbvralf.4 $e |- F/ x ps $.
-    cbvralf.5 $e |- ( x = y -> ( ph <-> ps ) ) $.
-    $( Rule used to change bound variables, using implicit substitution.  Usage
-       of this theorem is discouraged because it depends on ~ ax-13 .  Use the
-       weaker ~ cbvralfw when possible.  (Contributed by NM, 7-Mar-2004.)
-       (Revised by Mario Carneiro, 9-Oct-2016.)  (New usage is discouraged.) $)
-    cbvralf $p |- ( A. x e. A ph <-> A. y e. A ps ) $=
-      ( vz cv wcel wi wal wral wsb nfv nfcri nfim nfs1v sbequ12 imbi12d cbvalv1
-      weq eleq1w nfsb sbequ sbie bitrdi bitri df-ral 3bitr4i ) CLEMZANZCOZDLEMZ
-      BNZDOZACEPBDEPUPKLEMZACKQZNZKOUSUOVBCKUOKRUTVACCKEFSACKUATCKUEUNUTAVACKEU
-      FACKUBUCUDVBURKDUTVADDKEGSACKDHUGTURKRKDUEZUTUQVABKDEUFVCVAACDQBAKDCUHABC
-      DIJUIUJUCUDUKACEULBDEULUM $.
-
-    $( Rule used to change bound variables, using implicit substitution.  Usage
-       of this theorem is discouraged because it depends on ~ ax-13 .  Use the
-       weaker ~ cbvrexfw when possible.  (Contributed by FL, 27-Apr-2008.)
-       (Revised by Mario Carneiro, 9-Oct-2016.)  (New usage is discouraged.) $)
-    cbvrexf $p |- ( E. x e. A ph <-> E. y e. A ps ) $=
-      ( wn wral wrex nfn weq notbid cbvralf notbii dfrex2 3bitr4i ) AKZCELZKBKZ
-      DELZKACEMBDEMUBUDUAUCCDEFGADHNBCINCDOABJPQRACESBDEST $.
-  $}
-
   ${
     $d x y A $.
     cbvrmow.1 $e |- F/ y ph $.