move nfraldw and nfralw to main

metamath · Jan 16, 2024 · 8a5f7c6 · 8a5f7c6
1 parent 9b1afa2
commit 8a5f7c6
Showing 1 changed file with 53 additions and 53 deletions.
diff --git a/set.mm b/set.mm
@@ -28964,6 +28964,18 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
       ( cv wcel wi nfcri 19.21 r2allem ) ABCDEBGDHCGEHAICCBDFJKL $.
   $}
 
+  ${
+    $d x y $.
+    nfraldw.1 $e |- F/ y ph $.
+    nfraldw.2 $e |- ( ph -> F/_ x A ) $.
+    nfraldw.3 $e |- ( ph -> F/ x ps ) $.
+    $( Version of ~ nfrald with a disjoint variable condition, which does not
+       require ~ ax-13 .  (Contributed by Gino Giotto, 10-Jan-2024.) $)
+    nfraldw $p |- ( ph -> F/ x A. y e. A ps ) $=
+      ( wral cv wcel wi wal df-ral nfcvd nfeld nfimd nfald nfxfrd ) BDEIDJZEKZB
+      LZDMACBDENAUBCDFAUABCACTEACTOGPHQRS $.
+  $}
+
   ${
     nfrald.1 $e |- F/ y ph $.
     nfrald.2 $e |- ( ph -> F/_ x A ) $.
@@ -28976,6 +28988,17 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
       GRACDSUAACERUJGTUBABCUCUJHTUDUEUF $.
   $}
 
+  ${
+    $d x y $.
+    nfralw.1 $e |- F/_ x A $.
+    nfralw.2 $e |- F/ x ph $.
+    $( Version of ~ nfral with a disjoint variable condition, which does not
+       require ~ ax-13 .  (Contributed by Gino Giotto, 10-Jan-2024.) $)
+    nfralw $p |- F/ x A. y e. A ph $=
+      ( wral wnf wtru nftru wnfc a1i nfraldw mptru ) ACDGBHIABCDCJBDKIELABHIFLM
+      N $.
+  $}
+
   ${
     nfral.1 $e |- F/_ x A $.
     nfral.2 $e |- F/ x ph $.
@@ -32738,8 +32761,8 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
        substitution.  (Contributed by NM, 9-Nov-2012.) $)
     rspc2 $p |- ( ( A e. C /\ B e. D ) -> ( A. x e. C A. y e. D ph ->
                   ps ) ) $=
-      ( wcel wral nfcv nfral cv wceq rspc ralbidv sylan9 ) FHNAEIOZDHOCEIOZGINB
-      UCUDDFHCDEIDIPJQDRFSACEILUATCBEGIKMTUB $.
+      ( wcel wral nfcv nfralw cv wceq rspc ralbidv sylan9 ) FHNAEIOZDHOCEIOZGIN
+      BUCUDDFHCDEIDIPJQDRFSACEILUATCBEGIKMTUB $.
   $}
 
   ${
@@ -40126,7 +40149,7 @@ disjoint classes (see ~ disjdif ).  Part of proof of Corollary 6K of
     $( Rearrange restricted quantifiers.  (Contributed by NM, 26-Oct-2010.) $)
     raaan $p |- ( A. x e. A A. y e. A ( ph /\ ps ) <->
                   ( A. x e. A ph /\ A. y e. A ps ) ) $=
-      ( wa wral wb c0 wceq rzal pm5.1 syl12anc wne r19.28z ralbidv nfcv nfral
+      ( wa wral wb c0 wceq rzal pm5.1 syl12anc wne r19.28z ralbidv nfcv nfralw
       r19.27z bitrd pm2.61ine ) ABHDEIZCEIZACEIZBDEIZHZJZEKEKLUEUFUGUIUDCEMACEM
       BDEMUEUHNOEKPZUEAUGHZCEIUHUJUDUKCEABDEFQRAUGCEBCDECESGTUAUBUC $.
   $}
@@ -40175,10 +40198,10 @@ disjoint classes (see ~ disjdif ).  Part of proof of Corollary 6K of
                    -> ( A. x e. A A. y e. B ( ph /\ ps ) <->
                         ( A. x e. A ph /\ A. y e. B ps ) ) ) $=
       ( c0 wceq wb wa wn wo wral rzal adantr wne df-ne sylbir dfbi3 adantl nfcv
-      pm5.1 syl12anc r19.28z ralbidv nfral r19.27z sylan9bbr jaoi sylbi ) EIJZF
-      IJZKUMUNLZUMMZUNMZLZNABLDFOZCEOZACEOZBDFOZLZKZUMUNUAUOVDURUOUTVAVBVDUMUTU
-      NUSCEPQUMVAUNACEPQUNVBUMBDFPUBUTVCUDUEUQUTAVBLZCEOZUPVCUQFIRZUTVFKFISVGUS
-      VECEABDFGUFUGTUPEIRVFVCKEISAVBCEBCDFCFUCHUHUITUJUKUL $.
+      pm5.1 syl12anc r19.28z ralbidv nfralw r19.27z sylan9bbr jaoi sylbi ) EIJZ
+      FIJZKUMUNLZUMMZUNMZLZNABLDFOZCEOZACEOZBDFOZLZKZUMUNUAUOVDURUOUTVAVBVDUMUT
+      UNUSCEPQUMVAUNACEPQUNVBUMBDFPUBUTVCUDUEUQUTAVBLZCEOZUPVCUQFIRZUTVFKFISVGU
+      SVECEABDFGUFUGTUPEIRVFVCKEISAVBCEBCDFCFUCHUHUITUJUKUL $.
   $}
 
   ${
@@ -41655,11 +41678,11 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ).
     rexreusng $p |- ( A e. V -> ( E. x e. { A } ph <-> E! x e. { A } ph ) ) $=
       ( vy wcel csn wa wi wral wsbc cv wceq nfsbc1v nfv sbceq1a imbi12d ralsngf
       nfan nfim wrex wsb weq wreu eqidd dfsbcq2 anbi12d eqeq2 mpbiri nfcv nfs1v
-      nfral anbi1d eqeq1 ralbidv mpbird biantrud reu2 syl6bbr ) CDFZABCGZUAZVBA
-      ABEUBZHZBEUCZIZEVAJZBVAJZHABVAUDUTVHVBUTVHABCKZVCHZCELZMZIZEVAJZUTVNVIECK
-      ZVIHZCCMZIZVPCUEVMVRECDVPVQEVOVIEVIECNVIEOSVQEOTVKCMZVJVPVLVQVSVIVOVCVIVI
-      ECPABECUFUGVKCCUHQRUIVGVNBCDVMBEVABVAUJVJVLBVIVCBABCNABEUKSVLBOTULBLZCMZV
-      FVMEVAWAVDVJVEVLWAAVIVCABCPUMVTCVKUNQUORUPUQABEVAURUS $.
+      nfralw anbi1d eqeq1 ralbidv mpbird biantrud reu2 syl6bbr ) CDFZABCGZUAZVB
+      AABEUBZHZBEUCZIZEVAJZBVAJZHABVAUDUTVHVBUTVHABCKZVCHZCELZMZIZEVAJZUTVNVIEC
+      KZVIHZCCMZIZVPCUEVMVRECDVPVQEVOVIEVIECNVIEOSVQEOTVKCMZVJVPVLVQVSVIVOVCVIV
+      IECPABECUFUGVKCCUHQRUIVGVNBCDVMBEVABVAUJVJVLBVIVCBABCNABEUKSVLBOTULBLZCMZ
+      VFVMEVAWAVDVJVEVLWAAVIVCABCPUMVTCVKUNQUORUPUQABEVAURUS $.
   $}
 
   $( There is a set being the element of a singleton if and only if there is an
@@ -67203,13 +67226,13 @@ ordered pairs (for use in defining operations).  This is a special case
        Carneiro, 16-Dec-2013.)  (Revised by Mario Carneiro, 19-Mar-2015.) $)
     mpoeq123 $p |- ( ( A = D /\ A. x e. A ( B = E /\ A. y e. B C = F ) ) ->
                  ( x e. A , y e. B |-> C ) = ( x e. D , y e. E |-> F ) ) $=
-      ( vz wceq wral wa cv wcel coprab cmpo nfv nfra1 nfan wb nfral rsp pm5.32d
-      nfcv eqeq2 eleq2 anbi1d sylan9bbr anass 3bitr4g oprabbid df-mpo 3eqtr4g
-      syl6 ) CFJZDGJZEHJZBDKZLZACKZLZAMZCNZBMZDNZLIMZEJZLZABIOVBFNZVDGNZLVFHJZL
-      ZABIOABCDEPABFGHPVAVHVLABIUOUTAUOAQUSACRSUOUTBUOBQUSBACBCUDUPURBUPBQUQBDR
-      SUASVAIQVAVCVEVGLZLZVIVJVKLZLZVHVLUTVNVCVOLUOVPUTVCVMVOUTVCUSVMVOTUSACUBU
-      RVMVEVKLUPVOURVEVGVKURVEUQVGVKTUQBDUBEHVFUEUNUCUPVEVJVKDGVDUFUGUHUNUCUOVC
-      VIVOCFVBUFUGUHVCVEVGUIVIVJVKUIUJUKABICDEULABIFGHULUM $.
+      ( vz wceq wral wa cv wcel coprab cmpo nfv nfra1 nfan wb nfcv nfralw eqeq2
+      syl6 pm5.32d eleq2 anbi1d sylan9bbr anass 3bitr4g oprabbid df-mpo 3eqtr4g
+      rsp ) CFJZDGJZEHJZBDKZLZACKZLZAMZCNZBMZDNZLIMZEJZLZABIOVBFNZVDGNZLVFHJZLZ
+      ABIOABCDEPABFGHPVAVHVLABIUOUTAUOAQUSACRSUOUTBUOBQUSBACBCUAUPURBUPBQUQBDRS
+      UBSVAIQVAVCVEVGLZLZVIVJVKLZLZVHVLUTVNVCVOLUOVPUTVCVMVOUTVCUSVMVOTUSACUNUR
+      VMVEVKLUPVOURVEVGVKURVEUQVGVKTUQBDUNEHVFUCUDUEUPVEVJVKDGVDUFUGUHUDUEUOVCV
+      IVOCFVBUFUGUHVCVEVGUIVIVJVKUIUJUKABICDEULABIFGHULUM $.
   $}
 
   ${
@@ -513385,11 +513408,11 @@ Real and complex numbers (cont.)
        Scott Fenton, 28-Feb-2011.)  (Revised by Mario Carneiro,
        11-Dec-2016.) $)
     untsucf $p |- ( A. x e. A -. x e. x -> A. y e. suc A -. y e. y ) $=
-      ( wel wn wral csuc nfral cv wcel wceq wo elsuc elequ1 elequ2 bitrd notbid
-      nfv vex rspccv untelirr eleq1 eleq2 syl5ibrcom jaod syl5bi ralrimi ) AAEZ
-      FZACGZBBEZFZBCHZUJBACDUJBSIBJZUNKUOCKZUOCLZMUKUMUOCBTNUKUPUMUQUJUMAUOCAJU
-      OLZUIULURUIBAEULABAOABBPQRUAUKUMUQCCKZFACUBUQULUSUQULCUOKUSUOCUOUCUOCCUDQ
-      RUEUFUGUH $.
+      ( wel wn wral csuc nfv nfralw cv wcel wceq vex elsuc elequ1 elequ2 notbid
+      wo bitrd rspccv untelirr eleq1 eleq2 syl5ibrcom jaod syl5bi ralrimi ) AAE
+      ZFZACGZBBEZFZBCHZUJBACDUJBIJBKZUNLUOCLZUOCMZSUKUMUOCBNOUKUPUMUQUJUMAUOCAK
+      UOMZUIULURUIBAEULABAPABBQTRUAUKUMUQCCLZFACUBUQULUSUQULCUOLUSUOCUOUCUOCCUD
+      TRUEUFUGUH $.
   $}
 
   $( The null set is untangled.  (Contributed by Scott Fenton, 10-Mar-2011.)
@@ -629625,29 +629648,6 @@ standardize vectors to a length (norm) of one, but such definitions require
       OUNUPUQURUS $.
   $}
 
-  ${
-    $d x y $.
-    nfraldw.1 $e |- F/ y ph $.
-    nfraldw.2 $e |- ( ph -> F/_ x A ) $.
-    nfraldw.3 $e |- ( ph -> F/ x ps ) $.
-    $( Version of ~ nfrald with a disjoint variable condition, which does not
-       require ~ ax-13 .  (Contributed by Gino Giotto, 10-Jan-2024.) $)
-    nfraldw $p |- ( ph -> F/ x A. y e. A ps ) $=
-      ( wral cv wcel wi wal df-ral nfcvd nfeld nfimd nfald nfxfrd ) BDEIDJZEKZB
-      LZDMACBDENAUBCDFAUABCACTEACTOGPHQRS $.
-  $}
-
-  ${
-    $d x y $.
-    nfralw.1 $e |- F/_ x A $.
-    nfralw.2 $e |- F/ x ph $.
-    $( Version of ~ nfral with a disjoint variable condition, which does not
-       require ~ ax-13 .  (Contributed by Gino Giotto, 10-Jan-2024.) $)
-    nfralw $p |- F/ x A. y e. A ph $=
-      ( wral wnf wtru nftru wnfc a1i nfraldw mptru ) ACDGBHIABCDCJBDKIELABHIFLM
-      N $.
-  $}
-
   ${
     $d A y $.  $d x y $.
     $( Version of ~ nfra2 with a disjoint variable condition, which does not
@@ -637394,12 +637394,12 @@ group element in (1,2), contradicting ~ pell14qrgapw .  (Contributed by
     $( Set induction scheme without Infinity.  See comments at ~ setindtr .
        (Contributed by Stefan O'Rear, 28-Oct-2014.) $)
     setindtrs $p |- ( E. z ( Tr z /\ B e. z ) -> ch ) $=
-      ( va cv wtr wcel wa wex wi wral nfsab1 cvv setindtr dfss3 nfcv nfral nfim
-      cab wss weq raleq eleq1w imbi12d vex elab ralbii abid 3imtr4i chvar sylbi
-      mpg wb elex adantl exlimiv elabg syl mpbid ) FLZMZGVGNZOZFPZGADUFZNZCKLZV
-      LUGZVNVLNZQVKVMQKKFVLGUAVOELZVLNZEVNRZVPEVNVLUBVREDLZRZVTVLNZQVSVPQDKVSVP
-      DVRDEVNDVNUCADESUDADKSUEDKUHWAVSWBVPVREVTVNUIDKVLUJUKBEVTRAWAWBHVRBEVTABD
-      VQEULIUMUNADUOUPUQURUSVKGTNZVMCUTVJWCFVIWCVHGVGVAVBVCACDGTJVDVEVF $.
+      ( va cv wtr wcel wa wex wi wral nfsab1 cvv cab setindtr dfss3 nfcv nfralw
+      wss nfim weq raleq eleq1w imbi12d vex elab abid 3imtr4i chvarfv sylbi mpg
+      ralbii wb elex adantl exlimiv elabg syl mpbid ) FLZMZGVGNZOZFPZGADUAZNZCK
+      LZVLUFZVNVLNZQVKVMQKKFVLGUBVOELZVLNZEVNRZVPEVNVLUCVREDLZRZVTVLNZQVSVPQDKV
+      SVPDVRDEVNDVNUDADESUEADKSUGDKUHWAVSWBVPVREVTVNUIDKVLUJUKBEVTRAWAWBHVRBEVT
+      ABDVQEULIUMUSADUNUOUPUQURVKGTNZVMCUTVJWCFVIWCVHGVGVAVBVCACDGTJVDVEVF $.
   $}
 
   ${