ceqsrexv2 ceqsralv2 to main

metamath · Jan 12, 2025 · f2d0fc0 · f2d0fc0
1 parent 6774571
commit f2d0fc0
Showing 1 changed file with 16 additions and 46 deletions.
diff --git a/set.mm b/set.mm
@@ -33834,6 +33834,18 @@ general is seen either by substitution (when the variable ` V ` has no
       ( wcel cv wceq wa wrex r19.42v eleq1 adantr pm5.32ri bicomi baib ceqsrexv
       wb rexbiia pm5.32i 3bitr3i ) DEGZCHZDIZAJZJZCEKUCUFCEKZJUHUCBJUCUFCELUGUF
       CEUGUDEGZUFUIUFJUGUFUIUCUEUIUCSAUDDEMNOPQTUCUHBABCDEFRUAUB $.
+
+    $( Alternate elimitation of a restricted existential quantifier, using
+       implicit substitution.  (Contributed by Scott Fenton, 5-Sep-2017.) $)
+    ceqsrexv2 $p |- ( E. x e. B ( x = A /\ ph ) <-> ( A e. B /\ ps ) ) $=
+      ( ceqsrexbv ) ABCDEFG $.
+
+    $( Alternate elimination of a restricted universal quantifier, using
+       implicit substitution.  (Contributed by Scott Fenton, 7-Dec-2020.) $)
+    ceqsralv2 $p |- ( A. x e. B ( x = A -> ph ) <-> ( A e. B -> ps ) ) $=
+      ( cv wceq wi wral wcel wn wa wrex notbid ceqsrexv2 rexanali annim 3bitr3i
+      con4bii ) CGDHZAICEJZDEKZBIZUAALZMCENUCBLZMUBLUDLUEUFCDEUAABFOPUAACEQUCBR
+      ST $.
   $}
 
   ${
@@ -532424,15 +532436,6 @@ Real and complex numbers (cont.)
   brtpid3 $p |- A { C , D , <. A , B >. } B $=
     ( cop ctp wbr wcel opex tpid3 df-br mpbir ) ABCDABEZFZGMNHCDMABIJABNKL $.
 
-  ${
-    $d A x $.  $d B x $.  $d ps x $.
-    ceqsrexv2.1 $e |- ( x = A -> ( ph <-> ps ) ) $.
-    $( Alternate elimitation of a restricted existential quantifier, using
-       implicit substitution.  (Contributed by Scott Fenton, 5-Sep-2017.) $)
-    ceqsrexv2 $p |- ( E. x e. B ( x = A /\ ph ) <-> ( A e. B /\ ps ) ) $=
-      ( ceqsrexbv ) ABCDEFG $.
-  $}
-
   ${
     $d x V $.  $d A y $.  $d ps y $.  $d x y $.
     iota5f.1 $e |- F/ x ph $.
@@ -532447,17 +532450,6 @@ Real and complex numbers (cont.)
       GUEVEUTUNBVCDUMTUBUFVCDUQTUCBCIUGUHUIUJ $.
   $}
 
-  ${
-    $d x A $.  $d x B $.  $d ps x $.
-    ceqsralv2.1 $e |- ( x = A -> ( ph <-> ps ) ) $.
-    $( Alternate elimination of a restricted universal quantifier, using
-       implicit substitution.  (Contributed by Scott Fenton, 7-Dec-2020.) $)
-    ceqsralv2 $p |- ( A. x e. B ( x = A -> ph ) <-> ( A e. B -> ps ) ) $=
-      ( cv wceq wi wral wcel wn wa wrex notbid ceqsrexv2 rexanali annim 3bitr3i
-      con4bii ) CGDHZAICEJZDEKZBIZUAALZMCENUCBLZMUBLUDLUEUFCDEUAABFOPUAACEQUCBR
-      ST $.
-  $}
-
   $( A class is ordinal iff it is a subclass of ` On ` and transitive.
      (Contributed by Scott Fenton, 21-Nov-2021.) $)
   dford5 $p |- ( Ord A <-> ( A C_ On /\ Tr A ) ) $=
@@ -582175,38 +582167,16 @@ equivalence of domain elementhood (equivalence is not necessary as
       HUFUEUHPBUCUDQRSTUBUA $.
   $}
 
-  ${
-    $d A x $.  $d B x $.  $d ps x $.
-    ceqsrexv2TEMP.1 $e |- ( x = A -> ( ph <-> ps ) ) $.
-    $( Alternate elimitation of a restricted existential quantifier, using
-       implicit substitution.  (Contributed by Scott Fenton, 5-Sep-2017.) $)
-    ceqsrexv2TEMP $p |- ( E. x e. B ( x = A /\ ph ) <-> ( A e. B /\ ps ) ) $=
-      ( ceqsrexbv ) ABCDEFG $.
-  $}
-
-  ${
-    $d x A $.  $d x B $.  $d ps x $.
-    ceqsralv2TEMP.1 $e |- ( x = A -> ( ph <-> ps ) ) $.
-    $( Alternate elimination of a restricted universal quantifier, using
-       implicit substitution.  (Temporary: as soon as this Mathbox only PR is
-       accepted, I'll open a PR to place this to the main.  PM) (Contributed by
-       Scott Fenton, 7-Dec-2020.) $)
-    ceqsralv2TEMP $p |- ( A. x e. B ( x = A -> ph ) <-> ( A e. B -> ps ) ) $=
-      ( cv wceq wi wral wcel wrex notbid ceqsrexv2TEMP rexanali 3bitr3i con4bii
-      wn wa annim ) CGDHZAICEJZDEKZBIZUAARZSCELUCBRZSUBRUDRUEUFCDEUAABFMNUAACEO
-      UCBTPQ $.
-  $}
-
   ${
     $d A x y $.  $d B x y $.  $d R x y $.
     $( Two ways to say that an intersection of the identity relation with a
        Cartesian product is a subclass.  (Contributed by Peter Mazsa,
        12-Dec-2023.) $)
     ref5 $p |- ( ( _I i^i ( A X. B ) ) C_ R <-> A. x e. ( A i^i B ) x R x ) $=
-      ( vy cv wceq wbr wi wral wcel cid cxp cin wss equcom imbi1i ceqsralv2TEMP
-      ralbii breq2 bitr3i idinxpss ralin 3bitr4i ) AFZEFZGZUEUFDHZIZECJZABJUECK
-      UEUEDHZIZABJLBCMNDOUKABCNJUJULABUJUFUEGZUHIZECJULUNUIECUMUGUHEAPQSUHUKEUE
-      CUFUEUEDTRUASAEBCDUBUKABCUCUD $.
+      ( vy cv wceq wbr wral wcel cid cxp cin wss equcom imbi1i ralbii ceqsralv2
+      wi breq2 bitr3i idinxpss ralin 3bitr4i ) AFZEFZGZUEUFDHZSZECIZABIUECJUEUE
+      DHZSZABIKBCLMDNUKABCMIUJULABUJUFUEGZUHSZECIULUNUIECUMUGUHEAOPQUHUKEUECUFU
+      EUEDTRUAQAEBCDUBUKABCUCUD $.
   $}
 
   ${