rewrite restricted quantifier # 5 (metamath#4510)

* rewrite restricted quantifier # 5 * discouraged
avekens · Dec 30, 2024 · a1f39c0 · a1f39c0
1 parent 2d3605b
commit a1f39c0
Show file tree

Hide file tree

Showing 2 changed files with 34 additions and 93 deletions.
diff --git a/discouraged b/discouraged
@@ -11587,7 +11587,6 @@
 "opabid" is used by "brabidga".
 "opabid" is used by "ssopab2b".
 "opabresex2d" is used by "mptmpoopabbrdOLD".
-"opabresidOLD" is used by "mptresidOLD".
 "opelcn" is used by "axicn".
 "opelreal" is used by "ax1cn".
 "opelreal" is used by "axaddrcl".
@@ -14525,7 +14524,6 @@ New usage of "ajfval" is discouraged (2 uses).
 New usage of "ajmoi" is discouraged (1 uses).
 New usage of "ajval" is discouraged (0 uses).
 New usage of "al2imVD" is discouraged (0 uses).
-New usage of "alcomiwOLD" is discouraged (0 uses).
 New usage of "alephf1ALT" is discouraged (0 uses).
 New usage of "alexsubALT" is discouraged (0 uses).
 New usage of "alrim3con13v" is discouraged (1 uses).
@@ -16234,7 +16232,6 @@ New usage of "dochpolN" is discouraged (0 uses).
 New usage of "dochsordN" is discouraged (0 uses).
 New usage of "dochspocN" is discouraged (0 uses).
 New usage of "dom0OLD" is discouraged (0 uses).
-New usage of "domepOLD" is discouraged (0 uses).
 New usage of "dral1" is discouraged (10 uses).
 New usage of "dral1-o" is discouraged (4 uses).
 New usage of "dral1ALT" is discouraged (0 uses).
@@ -16703,7 +16700,6 @@ New usage of "fldhmsubcALTV" is discouraged (0 uses).
 New usage of "fldidomOLD" is discouraged (0 uses).
 New usage of "fncoOLD" is discouraged (0 uses).
 New usage of "fnexALT" is discouraged (0 uses).
-New usage of "fnresiOLD" is discouraged (0 uses).
 New usage of "fnsnfvOLD" is discouraged (0 uses).
 New usage of "footexALT" is discouraged (0 uses).
 New usage of "frgrwopreglem5ALT" is discouraged (0 uses).
@@ -17876,7 +17872,6 @@ New usage of "mpteq2dvaOLD" is discouraged (0 uses).
 New usage of "mpteq2iaOLD" is discouraged (0 uses).
 New usage of "mptmpoopabbrdOLD" is discouraged (1 uses).
 New usage of "mptmpoopabovdOLD" is discouraged (1 uses).
-New usage of "mptresidOLD" is discouraged (0 uses).
 New usage of "mptssALT" is discouraged (0 uses).
 New usage of "mpv" is discouraged (1 uses).
 New usage of "mrelatglbALT" is discouraged (0 uses).
@@ -18329,7 +18324,6 @@ New usage of "onsetreclem2" is discouraged (1 uses).
 New usage of "onsetreclem3" is discouraged (1 uses).
 New usage of "opabid" is discouraged (2 uses).
 New usage of "opabresex2d" is discouraged (1 uses).
-New usage of "opabresidOLD" is discouraged (1 uses).
 New usage of "opelcn" is discouraged (1 uses).
 New usage of "opelopab4" is discouraged (0 uses).
 New usage of "opelreal" is discouraged (8 uses).
@@ -18704,7 +18698,6 @@ New usage of "pwfilemOLD" is discouraged (0 uses).
 New usage of "pwsnOLD" is discouraged (0 uses).
 New usage of "pwtrVD" is discouraged (0 uses).
 New usage of "pwtrrVD" is discouraged (0 uses).
-New usage of "pwundifOLD" is discouraged (0 uses).
 New usage of "pwunssOLD" is discouraged (0 uses).
 New usage of "pythi" is discouraged (0 uses).
 New usage of "qexALT" is discouraged (1 uses).
@@ -19724,7 +19717,6 @@ Proof modification of "aecoms-o" is discouraged (16 steps).
 Proof modification of "aev-o" is discouraged (117 steps).
 Proof modification of "aevdemo" is discouraged (69 steps).
 Proof modification of "al2imVD" is discouraged (48 steps).
-Proof modification of "alcomiwOLD" is discouraged (59 steps).
 Proof modification of "alephf1ALT" is discouraged (47 steps).
 Proof modification of "alexsubALT" is discouraged (869 steps).
 Proof modification of "alrim3con13v" is discouraged (74 steps).
@@ -20194,7 +20186,6 @@ Proof modification of "dmfexALT" is discouraged (25 steps).
 Proof modification of "dmmpogaOLD" is discouraged (31 steps).
 Proof modification of "dmtrclfvRP" is discouraged (46 steps).
 Proof modification of "dom0OLD" is discouraged (40 steps).
-Proof modification of "domepOLD" is discouraged (51 steps).
 Proof modification of "dral1ALT" is discouraged (34 steps).
 Proof modification of "dral1vOLD" is discouraged (36 steps).
 Proof modification of "dral2-o" is discouraged (14 steps).
@@ -20503,7 +20494,6 @@ Proof modification of "fineqvacALT" is discouraged (40 steps).
 Proof modification of "fldidomOLD" is discouraged (34 steps).
 Proof modification of "fncoOLD" is discouraged (95 steps).
 Proof modification of "fnexALT" is discouraged (111 steps).
-Proof modification of "fnresiOLD" is discouraged (25 steps).
 Proof modification of "fnsnfvOLD" is discouraged (74 steps).
 Proof modification of "footexALT" is discouraged (2161 steps).
 Proof modification of "frege10" is discouraged (27 steps).
@@ -20913,7 +20903,6 @@ Proof modification of "mpteq2dvaOLD" is discouraged (10 steps).
 Proof modification of "mpteq2iaOLD" is discouraged (37 steps).
 Proof modification of "mptmpoopabbrdOLD" is discouraged (247 steps).
 Proof modification of "mptmpoopabovdOLD" is discouraged (89 steps).
-Proof modification of "mptresidOLD" is discouraged (28 steps).
 Proof modification of "mptssALT" is discouraged (57 steps).
 Proof modification of "mrelatglbALT" is discouraged (66 steps).
 Proof modification of "mrelatlubALT" is discouraged (76 steps).
@@ -21018,7 +21007,6 @@ Proof modification of "onfrALTlem5VD" is discouraged (320 steps).
 Proof modification of "onnevOLD" is discouraged (26 steps).
 Proof modification of "onomeneqOLD" is discouraged (251 steps).
 Proof modification of "opabresex2d" is discouraged (48 steps).
-Proof modification of "opabresidOLD" is discouraged (50 steps).
 Proof modification of "opelopab4" is discouraged (69 steps).
 Proof modification of "opidon2OLD" is discouraged (80 steps).
 Proof modification of "opidonOLD" is discouraged (198 steps).
@@ -21099,7 +21087,6 @@ Proof modification of "pwfilemOLD" is discouraged (197 steps).
 Proof modification of "pwsnOLD" is discouraged (164 steps).
 Proof modification of "pwtrVD" is discouraged (110 steps).
 Proof modification of "pwtrrVD" is discouraged (110 steps).
-Proof modification of "pwundifOLD" is discouraged (49 steps).
 Proof modification of "pwunssOLD" is discouraged (61 steps).
 Proof modification of "qexALT" is discouraged (64 steps).
 Proof modification of "quoremnn0ALT" is discouraged (360 steps).

diff --git a/set.mm b/set.mm
@@ -17006,13 +17006,6 @@ variables and no wff metavariables (see ~ ax12wdemo for an example of
       ) ADGZCGBEGZCGZUADGACGDGSTCSTABDEFHIJUADKTADCBAEDBALDEDEMABFNOPQR $.
     $( $j usage 'alcomiw' avoids 'ax-8' 'ax-9' 'ax-10' 'ax-11' 'ax-12'
        'ax-13'; $)
-    $( Obsolete version of ~ alcomiw as of 28-Dec-2023.  (Contributed by NM,
-       10-Apr-2017.)  (Proof shortened by Wolf Lammen, 12-Jul-2022.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    alcomiwOLD $p |- ( A. x A. y ph -> A. y A. x ph ) $=
-      ( wal weq biimpd cbvalivw alimi ax-5 biimprd equcoms spimvw 2alimi 3syl
-      wi ) ADGZCGBEGZCGZUADGACGDGSTCABDEDEHZABFIJKUADLTADCBAEDBARDEUBABFMNOPQ
-      $.
   $}
 
   ${
@@ -29663,6 +29656,40 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
       NUGUICDEFPUBCELQUDUESRT $.
   $}
 
+  ${
+    $d x A $.  $d x B $.
+    $( Two ways to say " ` A ` belongs to ` B ` ".  (Contributed by NM,
+       22-Nov-1994.) $)
+    risset $p |- ( A e. B <-> E. x e. B x = A ) $=
+      ( cv wcel wceq wa wex wrex exancom df-rex dfclel 3bitr4ri ) ADZCEZNBFZGAH
+      POGAHPACIBCEOPAJPACKABCLM $.
+
+    $( A definition of ` -. A e. B ` .  (Contributed by Thierry Arnoux,
+       20-Nov-2023.)  (Proof shortened by SN, 23-Jan-2024.)  (Proof shortened
+       by Wolf Lammen, 3-Nov-2024.) $)
+    nelb $p |- ( -. A e. B <-> A. x e. B x =/= A ) $=
+      ( cv wceq wrex wne wral wcel df-ne ralbii ralnex bitr2i risset xchnxbir
+      wn ) ADZBEZACFZQBGZACHZBCIUARPZACHSPTUBACQBJKRACLMABCNO $.
+
+    $( Obsolete version of ~ nelb as of 3-Nov-2024.  (Contributed by Thierry
+       Arnoux, 20-Nov-2023.)  (Proof shortened by SN, 23-Jan-2024.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    nelbOLD $p |- ( -. A e. B <-> A. x e. B x =/= A ) $=
+      ( cv wne wral wcel wn wceq wrex df-ne ralbii ralnex bitri risset xchbinxr
+      bicomi ) ADZBEZACFZBCGZHTRBIZACJZUATUBHZACFUCHSUDACRBKLUBACMNABCOPQ $.
+  $}
+
+  ${
+    $d x y A $.  $d x ps $.  $d y ph $.
+    rspw.1 $e |- ( x = y -> ( ph <-> ps ) ) $.
+    $( Restricted specialization.  Weak version of ~ rsp , requiring ~ ax-8 ,
+       but not ~ ax-12 .  (Contributed by Gino Giotto, 3-Oct-2024.) $)
+    rspw $p |- ( A. x e. A ph -> ( x e. A -> ph ) ) $=
+      ( wral cv wcel wi wal df-ral weq eleq1w imbi12d spw sylbi ) ACEGCHEIZAJZC
+      KSACELSDHEIZBJCDCDMRTABCDENFOPQ $.
+    $( $j usage 'rspw' avoids 'ax-10' 'ax-11' 'ax-12'; $)
+  $}
+
   $( Extend wff notation to include restricted existential uniqueness. $)
   wreu $a wff E! x e. A ph $.
 
@@ -29711,17 +29738,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 ) } $.
 
-  ${
-    $d x y A $.  $d x ps $.  $d y ph $.
-    rspw.1 $e |- ( x = y -> ( ph <-> ps ) ) $.
-    $( Restricted specialization.  Weak version of ~ rsp , requiring ~ ax-8 ,
-       but not ~ ax-12 .  (Contributed by Gino Giotto, 3-Oct-2024.) $)
-    rspw $p |- ( A. x e. A ph -> ( x e. A -> ph ) ) $=
-      ( wral cv wcel wi wal df-ral weq eleq1w imbi12d spw sylbi ) ACEGCHEIZAJZC
-      KSACELSDHEIZBJCDCDMRTABCDENFOPQ $.
-    $( $j usage 'rspw' avoids 'ax-10' 'ax-11' 'ax-12'; $)
-  $}
-
   $( Restricted specialization.  (Contributed by NM, 17-Oct-1996.) $)
   rsp $p |- ( A. x e. A ph -> ( x e. A -> ph ) ) $=
     ( wral cv wcel wi wal df-ral sp sylbi ) ABCDBECFAGZBHLABCILBJK $.
@@ -30070,29 +30086,6 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
        'ax-13' 'ax-ext'; $)
   $}
 
-  ${
-    $d x A $.  $d x B $.
-    $( Two ways to say " ` A ` belongs to ` B ` ".  (Contributed by NM,
-       22-Nov-1994.) $)
-    risset $p |- ( A e. B <-> E. x e. B x = A ) $=
-      ( cv wcel wceq wa wex wrex exancom df-rex dfclel 3bitr4ri ) ADZCEZNBFZGAH
-      POGAHPACIBCEOPAJPACKABCLM $.
-
-    $( A definition of ` -. A e. B ` .  (Contributed by Thierry Arnoux,
-       20-Nov-2023.)  (Proof shortened by SN, 23-Jan-2024.)  (Proof shortened
-       by Wolf Lammen, 3-Nov-2024.) $)
-    nelb $p |- ( -. A e. B <-> A. x e. B x =/= A ) $=
-      ( cv wceq wrex wne wral wcel df-ne ralbii ralnex bitr2i risset xchnxbir
-      wn ) ADZBEZACFZQBGZACHZBCIUARPZACHSPTUBACQBJKRACLMABCNO $.
-
-    $( Obsolete version of ~ nelb as of 3-Nov-2024.  (Contributed by Thierry
-       Arnoux, 20-Nov-2023.)  (Proof shortened by SN, 23-Jan-2024.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    nelbOLD $p |- ( -. A e. B <-> A. x e. B x =/= A ) $=
-      ( cv wne wral wcel wn wceq wrex df-ne ralbii ralnex bitri risset xchbinxr
-      bicomi ) ADZBEZACFZBCGZHTRBIZACJZUATUBHZACFUCHSUDACRBKLUBACMNABCOPQ $.
-  $}
-
   ${
     $d x y $.  $d y A $.
     $( Commutation of restricted and unrestricted existential quantifiers.
@@ -52578,13 +52571,6 @@ necessary if all involved classes exist as sets (i.e. are not proper
       LVDVAVENLVCVFVGVHWMVPVIVJVKVLVGVMVNVO $.
   $}
 
-  $( Obsolete proof of ~ pwundif as of 26-Dec-2023.  (Contributed by NM,
-     25-Mar-2007.)  (Proof shortened by Thierry Arnoux, 20-Dec-2016.)
-     (Proof modification is discouraged.)  (New usage is discouraged.) $)
-  pwundifOLD $p |- ~P ( A u. B ) = ( ( ~P ( A u. B ) \ ~P A ) u. ~P A ) $=
-    ( cun cpw cdif undif1 wss wceq pwunss unss mpbir simpli ssequn2 mpbi eqtr2i
-    wa ) ABCDZADZERCQRCZQQRFRQGZSQHTBDZQGZTUBPRUACQGABIRUAQJKLRQMNO $.
-
   $( The power class of the union of two classes equals the union of their
      power classes, iff one class is a subclass of the other.  Part of Exercise
      7(b) of [Enderton] p. 28.  (Contributed by NM, 23-Nov-2003.) $)
@@ -55950,14 +55936,6 @@ ordered pairs as classes (in set.mm, the Kuratowski encoding).  A more
       ( vx vy cep cdm cvv wceq cv wcel eqv wbr wex wel el epel exbii mpbir eldm
       vex mpgbir ) CDZEFAGZTHZAATIUBUABGCJZBKZUDABLZBKABMUCUEBBUANOPBUACARQPS
       $.
-
-    $( Obsolete proof of ~ dmep as of 26-Dec-2023.  (Contributed by Scott
-       Fenton, 27-Oct-2010.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    domepOLD $p |- dom _E = _V $=
-      ( vx vy weq cab cv cep wbr wex cvv cdm equid wel el exbii mpbir 2th abbii
-      epel df-v df-dm 3eqtr4ri ) AACZADAEZBEFGZBHZADIFJUBUEAUBUEAKUEABLZBHABMUD
-      UFBBUCRNOPQASABFTUA $.
   $}
 
   ${
@@ -56952,23 +56930,6 @@ the restriction (of the relation) to the singleton containing this
       GCAHIACJABOKACBLACBOMN $.
   $}
 
-  ${
-    $d A x y $.
-    $( Obsolete version of ~ opabresid as of 26-Dec-2023.  (Contributed by FL,
-       25-Apr-2012.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    opabresidOLD $p |- { <. x , y >. | ( x e. A /\ y = x ) } = ( _I |` A ) $=
-      ( weq copab cres cv wcel cid resopab equcom opabbii eqtr4i reseq1i eqtr3i
-      wa df-id ) BADZABEZCFAGCHRPABEICFRABCJSICSABDZABEIRTABBAKLABQMNO $.
-
-    $( Obsolete version of ~ mptresid as of 26-Dec-2023.  (Contributed by FL,
-       25-Apr-2012.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    mptresidOLD $p |- ( x e. A |-> x ) = ( _I |` A ) $=
-      ( vy cv cmpt wcel weq wa copab cid cres df-mpt opabresidOLD eqtri ) ABADZ
-      EOBFCAGHACIJBKACBOLACBMN $.
-  $}
-
   $( The domain of a restricted identity function.  (Contributed by NM,
      27-Aug-2004.) $)
   dmresi $p |- dom ( _I |` A ) = A $=
@@ -62692,13 +62653,6 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ).
   fnresi $p |- ( _I |` A ) Fn A $=
     ( cid cvv wfn wss cres idfn ssv fnssres mp2an ) BCDACEBAFADGAHCABIJ $.
 
-  $( Obsolete proof of ~ fnresi as of 27-Dec-2023.  (Contributed by NM,
-     27-Aug-2004.)  (Proof modification is discouraged.)
-     (New usage is discouraged.) $)
-  fnresiOLD $p |- ( _I |` A ) Fn A $=
-    ( cid cres wfn wfun cdm wceq funi funres ax-mp dmresi df-fn mpbir2an ) BACZ
-    ADNEZNFAGBEOHABIJAKNALM $.
-
   $( The image of a function's domain is its range.  (Contributed by NM,
      4-Nov-2004.)  (Proof shortened by Andrew Salmon, 17-Sep-2011.) $)
   fnima $p |- ( F Fn A -> ( F " A ) = ran F ) $=