minimize ax-13 usage (#3796)

metamath · Jan 27, 2024 · 0cb0f66 · 0cb0f66
1 parent 1d9443c
commit 0cb0f66
Showing 1 changed file with 18 additions and 18 deletions.
diff --git a/set.mm b/set.mm
@@ -31514,10 +31514,10 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
     $( Implicit to explicit substitution that swaps variables in a quantified
        expression.  (Contributed by NM, 5-Sep-2004.) $)
     sbralie $p |- ( A. x e. y ph <-> [ y / x ] A. y e. x ps ) $=
-      ( vz cv wral wsb cbvralsv sbbii raleq sbievw sbco2vv wb weq equcoms bitri
-      bicomd ralbii 3bitrri ) BDCGZHZCDIBDFIZFUBHZCDIUDFDGZHZACUFHZUCUECDBDFUBJ
-      KUEUGCDUDFUBUFLMUGUDFCIZCUFHUHUDFCUFJUIACUFUIBDCIABDCFNBADCBAOCDCDPABESQM
-      RTRUA $.
+      ( vz cv wral wsb cbvralsvw sbbii raleq sbievw sbco2vv wb weq bicomd bitri
+      equcoms ralbii 3bitrri ) BDCGZHZCDIBDFIZFUBHZCDIUDFDGZHZACUFHZUCUECDBDFUB
+      JKUEUGCDUDFUBUFLMUGUDFCIZCUFHUHUDFCUFJUIACUFUIBDCIABDCFNBADCBAOCDCDPABEQS
+      MRTRUA $.
   $}
 
   ${
@@ -34304,7 +34304,7 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
        24-Oct-2006.) $)
     reu8 $p |- ( E! x e. A ph <-> E. x e. A ( ph /\
                 A. y e. A ( ps -> x = y ) ) ) $=
-      ( wreu weq wb wral wrex wi wa cbvreuv reu6 cv wcel ralbii wal syl5bb a1i
+      ( wreu weq wb wral wrex wi wa cbvreuvw reu6 cv wcel ralbii wal syl5bb a1i
       dfbi2 ancom equcom imbi2i biimt df-ral bi2.04 albii eleq1w imbi12d bicomd
       equcoms equsalvw 3bitrri syl6bb anbi12d r19.26 syl6rbbr rexbiia 3bitri )
       ACEGBDEGBDCHZIZDEJZCEKABCDHZLZDEJZMZCEKABCDEFNBDCEOVDVHCEVDBVBLZVBBLZMZDE
@@ -34324,12 +34324,12 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
     rmo3f $p |- ( E* x e. A ph <->
                A. x e. A A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) ) $=
       ( cv wcel wa wsb wi wral wal anbi1i bitri 3bitri impexp albii df-ral wrmo
-      wmo weq df-rmo sban clelsb3f anbi2i an4 ancom imbi1i nfcri r19.21 3bitr2i
-      nfan mo3 3bitr4i ) ABDUABHDIZAJZBUBZAABCKZJZBCUCZLZCDMZBDMZABDUDURURBCKZJ
-      ZVBLZCNZBNUQVDLZBNUSVEVIVJBVICHDIZUQVCLZLZCNVLCDMVJVHVMCVHVKUQJZVAJZVBLVN
-      VCLVMVGVOVBVGURVKUTJZJUQVKJZVAJVOVFVPURVFUQBCKZUTJVPUQABCUEVRVKUTBCDEUFOP
-      UGUQAVKUTUHVQVNVAUQVKUIOQUJVNVAVBRVKUQVCRQSVLCDTUQVCCDCBDFUKZULUMSURBCUQA
-      CVSGUNUOVDBDTUPP $.
+      wmo weq df-rmo sban clelsb3fw anbi2i an4 ancom imbi1i r19.21 3bitr2i nfan
+      nfcri mo3 3bitr4i ) ABDUABHDIZAJZBUBZAABCKZJZBCUCZLZCDMZBDMZABDUDURURBCKZ
+      JZVBLZCNZBNUQVDLZBNUSVEVIVJBVICHDIZUQVCLZLZCNVLCDMVJVHVMCVHVKUQJZVAJZVBLV
+      NVCLVMVGVOVBVGURVKUTJZJUQVKJZVAJVOVFVPURVFUQBCKZUTJVPUQABCUEVRVKUTBCDEUFO
+      PUGUQAVKUTUHVQVNVAUQVKUIOQUJVNVAVBRVKUQVCRQSVLCDTUQVCCDCBDFUNZUKULSURBCUQ
+      ACVSGUMUOVDBDTUPP $.
   $}
 
   ${
@@ -34344,9 +34344,9 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
        8-Oct-2017.) $)
     rmo4f $p |- ( E* x e. A ph <->
                A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) ) $=
-      ( wrmo wsb wa weq wi wral nfv rmo3f sbie anbi2i imbi1i 2ralbii bitri ) AC
-      EJAACDKZLZCDMZNZDEOCEOABLZUENZDEOCEOACDEFGADPQUFUHCDEEUDUGUEUCBAABCDHIRST
-      UAUB $.
+      ( wrmo wsb wa weq wi wral nfv rmo3f sbiev anbi2i imbi1i 2ralbii bitri ) A
+      CEJAACDKZLZCDMZNZDEOCEOABLZUENZDEOCEOACDEFGADPQUFUHCDEEUDUGUEUCBAABCDHIRS
+      TUAUB $.
   $}
 
   ${
@@ -34574,9 +34574,9 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
     $( Double restricted quantification with "at most one", analogous to
        ~ 2moex .  (Contributed by Alexander van der Vekens, 17-Jun-2017.) $)
     2rmorex $p |- ( E* x e. A E. y e. B ph -> A. y e. B E* x e. A ph ) $=
-      ( wrex wrmo nfcv nfre1 nfrmo wi wral cv wcel rmoim rspe ralrimivw ralrimi
-      ex syl11 ) ACEFZBDGZABDGZCEUACBDCDHACEIJAUAKZBDLUBUCCMENZAUABDOUEUDBDUEAU
-      AACEPSQTR $.
+      ( wrex wrmo nfcv nfre1 nfrmow wi wral cv wcel rmoim rspe ex syl11 ralrimi
+      ralrimivw ) ACEFZBDGZABDGZCEUACBDCDHACEIJAUAKZBDLUBUCCMENZAUABDOUEUDBDUEA
+      UAACEPQTRS $.
 
     $( Lemma for ~ 2reu5 .  Note that ` E! x e. A E! y e. B ph ` does not mean
        "there is exactly one ` x ` in ` A ` and exactly one ` y ` in ` B ` such
@@ -34642,7 +34642,7 @@ that existential restriction in the last conjunct (the "at most one"
     $( Double restricted quantification with existential uniqueness, analogous
        to ~ 2euex .  (Contributed by Alexander van der Vekens, 24-Jun-2017.) $)
     2reurex $p |- ( E! x e. A E. y e. B ph -> E. y e. B E! x e. A ph ) $=
-      ( wrex wreu wrmo wa reu5 rexcom nfcv nfre1 nfrmo cv wcel wi wral impcom
+      ( wrex wreu wrmo wa reu5 rexcom nfcv nfre1 nfrmow cv wcel wi wral impcom
       ex rspe ralrimivw rmoim syl rmo5 sylib reximdai syl5bi sylbi ) ACEFZBDGUJ
       BDFZUJBDHZIABDGZCEFZUJBDJULUKUNUKABDFZCEFULUNABCDEKULUOUMCEUJCBDCDLACEMNU
       LCOEPZUOUMQZULUPIABDHZUQUPULURUPAUJQZBDRULURQUPUSBDUPAUJACEUATUBAUJBDUCUD