more eqab* renamings (#4679)

metamath · Feb 27, 2025 · 37f6402 · 37f6402
1 parent 03c5d4e
commit 37f6402
Show file tree

Hide file tree

Showing 3 changed files with 1,152 additions and 1,151 deletions.
diff --git a/changes-set.txt b/changes-set.txt
@@ -140,9 +140,9 @@ Date      Old       New         Notes
 19-Feb-25 isdrngd   [same]      removed extra hypothesis
 15-Feb-25 abeq2f    eqabf
 15-Feb-25 rabeq2i   reqabi
-15-Feb-25 abeq1i    eqabci
-15-Feb-25 abeq2i    eqabi
-15-Feb-25 abeq2d    eqabd
+15-Feb-25 abeq1i    eqabrci
+15-Feb-25 abeq2i    eqabri
+15-Feb-25 abeq2d    eqabrd
 15-Feb-25 abeq2w    eqabbw
 15-Feb-25 abeq1     eqabbc      Commuted form of eqabb
 15-Feb-25 abeq2     eqabb       Basic closed form

diff --git a/nf.mm b/nf.mm
@@ -21382,26 +21382,26 @@ atomic formula (class version of ~ elsb2 ).  (Contributed by Jim
   $}
 
   ${
-    abeqi.1 $e |- A = { x | ph } $.
+    eqabri.1 $e |- A = { x | ph } $.
     $( Equality of a class variable and a class abstraction (inference rule).
        (Contributed by NM, 3-Apr-1996.) $)
-    eqabi $p |- ( x e. A <-> ph ) $=
+    eqabri $p |- ( x e. A <-> ph ) $=
       ( cv wcel cab eleq2i abid bitri ) BEZCFKABGZFACLKDHABIJ $.
   $}
 
   ${
-    abeqri.1 $e |- { x | ph } = A $.
+    eqabcri.1 $e |- { x | ph } = A $.
     $( Equality of a class variable and a class abstraction (inference rule).
        (Contributed by NM, 31-Jul-1994.) $)
-    eqabci $p |- ( ph <-> x e. A ) $=
+    eqabcri $p |- ( ph <-> x e. A ) $=
       ( cv cab wcel abid eleq2i bitr3i ) ABEZABFZGKCGABHLCKDIJ $.
   $}
 
   ${
-    abeqd.1 $e |- ( ph -> A = { x | ps } ) $.
+    eqabrd.1 $e |- ( ph -> A = { x | ps } ) $.
     $( Equality of a class variable and a class abstraction (deduction).
        (Contributed by NM, 16-Nov-1995.) $)
-    eqabd $p |- ( ph -> ( x e. A <-> ps ) ) $=
+    eqabrd $p |- ( ph -> ( x e. A <-> ps ) ) $=
       ( cv wcel cab eleq2d abid syl6bb ) ACFZDGLBCHZGBADMLEIBCJK $.
   $}
 
@@ -24064,7 +24064,7 @@ atomic formula (class version of ~ elsb2 ).  (Contributed by Jim
   $( An "identity" law of concretion for restricted abstraction.  Special case
      of Definition 2.1 of [Quine] p. 16.  (Contributed by NM, 9-Oct-2003.) $)
   rabid $p |- ( x e. { x e. A | ph } <-> ( x e. A /\ ph ) ) $=
-    ( cv wcel wa crab df-rab eqabi ) BDCEAFBABCGABCHI $.
+    ( cv wcel wa crab df-rab eqabri ) BDCEAFBABCGABCHI $.
 
   ${
     $d x A $.
@@ -24695,7 +24695,7 @@ atomic formula (class version of ~ elsb2 ).  (Contributed by Jim
   $( All setvar variables are sets (see ~ isset ).  Theorem 6.8 of [Quine]
      p. 43.  (Contributed by NM, 5-Aug-1993.) $)
   vex $p |- x e. _V $=
-    ( cv cvv wcel wceq eqid df-v eqabi mpbir ) ABZCDJJEZJFKACAGHI $.
+    ( cv cvv wcel wceq eqid df-v eqabri mpbir ) ABZCDJJEZJFKACAGHI $.
 
   ${
     $d x A $.
@@ -27875,9 +27875,9 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
     $( Composition law for chained substitutions into a class.  (Contributed by
        NM, 10-Nov-2005.) $)
     csbco $p |- [_ A / y ]_ [_ y / x ]_ B = [_ A / x ]_ B $=
-      ( vz cv csb wcel wsbc cab df-csb eqabi sbcbii sbcco bitri abbii 3eqtr4i )
-      EFZABFZDGZHZBCIZEJRDHZACIZEJBCTGACDGUBUDEUBUCASIZBCIUDUAUEBCUEETAESDKLMUC
-      ABCNOPBECTKAECDKQ $.
+      ( vz cv csb wcel wsbc cab df-csb eqabri sbcbii sbcco bitri abbii 3eqtr4i
+      ) EFZABFZDGZHZBCIZEJRDHZACIZEJBCTGACDGUBUDEUBUCASIZBCIUDUAUEBCUEETAESDKLM
+      UCABCNOPBECTKAECDKQ $.
   $}
 
   ${
@@ -28284,11 +28284,11 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
        23-Nov-2005.)  (Proof shortened by Mario Carneiro, 10-Nov-2016.) $)
     csbnestgf $p |- ( ( A e. V /\ A. y F/_ x C ) ->
          [_ A / x ]_ [_ B / y ]_ C = [_ [_ A / x ]_ B / y ]_ C ) $=
-      ( vz wcel wnfc wal wa cv csb wsbc cab cvv wceq elex df-csb eqabi wnf nfcr
-      sbcbii wb alimi sbcnestgf sylan2 syl5bb abbidv sylan 3eqtr4g ) CFHZAEIZBJ
-      ZKGLZBDEMZHZACNZGOZUOEHZBACDMZNZGOZACUPMBVAEMULCPHZUNUSVCQCFRVDUNKZURVBGU
-      RUTBDNZACNZVEVBUQVFACVFGUPBGDESTUCUNVDUTAUAZBJVGVBUDUMVHBAGEUBUEUTABCDPUF
-      UGUHUIUJAGCUPSBGVAESUK $.
+      ( vz wcel wnfc wal wa cv csb wsbc cab cvv wceq elex df-csb eqabri wb nfcr
+      sbcbii wnf alimi sbcnestgf sylan2 syl5bb abbidv sylan 3eqtr4g ) CFHZAEIZB
+      JZKGLZBDEMZHZACNZGOZUOEHZBACDMZNZGOZACUPMBVAEMULCPHZUNUSVCQCFRVDUNKZURVBG
+      URUTBDNZACNZVEVBUQVFACVFGUPBGDESTUCUNVDUTAUDZBJVGVBUAUMVHBAGEUBUEUTABCDPU
+      FUGUHUIUJAGCUPSBGVAESUK $.
 
     $d x ph $.
     $( Nest the composition of two substitutions.  (Contributed by NM,
@@ -32675,8 +32675,8 @@ fewer connectives (but probably less intuitive to understand).
     $( Subclass relationship for power class.  (Contributed by NM,
        21-Jun-2009.) $)
     pwss $p |- ( ~P A C_ B <-> A. x ( x C_ A -> x e. B ) ) $=
-      ( cpw wss cv wcel wi wal dfss2 df-pw eqabi imbi1i albii bitri ) BDZCEAFZP
-      GZQCGZHZAIQBEZSHZAIAPCJTUBARUASUAAPABKLMNO $.
+      ( cpw wss cv wcel wi wal dfss2 df-pw eqabri imbi1i albii bitri ) BDZCEAFZ
+      PGZQCGZHZAIQBEZSHZAIAPCJTUBARUASUAAPABKLMNO $.
   $}
 
 
@@ -32757,7 +32757,7 @@ fewer connectives (but probably less intuitive to understand).
     $( There is only one element in a singleton.  Exercise 2 of [TakeutiZaring]
        p. 15.  (Contributed by NM, 5-Aug-1993.) $)
     elsn $p |- ( x e. { A } <-> x = A ) $=
-      ( cv wceq csn df-sn eqabi ) ACBDABEABFG $.
+      ( cv wceq csn df-sn eqabri ) ACBDABEABFG $.
   $}
 
   ${
@@ -33770,8 +33770,8 @@ fewer connectives (but probably less intuitive to understand).
     $( The singleton of a class is a subset of its power class.  (Contributed
        by NM, 5-Aug-1993.) $)
     snsspw $p |- { A } C_ ~P A $=
-      ( vx csn cpw cv wceq wss wcel eqimss elsn df-pw eqabi 3imtr4i ssriv ) BAC
-      ZADZBEZAFQAGZQOHQPHQAIBAJRBPBAKLMN $.
+      ( vx csn cpw cv wceq wss wcel eqimss elsn df-pw eqabri 3imtr4i ssriv ) BA
+      CZADZBEZAFQAGZQOHQPHQAIBAJRBPBAKLMN $.
   $}
 
   ${
@@ -36316,10 +36316,10 @@ Kuratowski ordered pairs (continued)
     $( Cardinal one is a set.  (Contributed by SF, 12-Jan-2015.) $)
     1cex $p |- 1c e. _V $=
       ( vy vx vw vz c1c cvv wcel wel weq wb wal wex ax-1c cv isset bitri bibi2i
-      wceq albii exbii csn cab df-1c eqeq2i eqabb dfcleq df-sn eqabi mpbir ) EF
-      GZABHZCAHZCDIZJZCKZDLZJZAKZBLZBADCMUJBNZERZBLUSBEOVAURBVAUKANZDNZUAZRZDLZ
-      JZAKZURVAUTVFAUBZRVHEVIUTADUCUDVFAUTUEPVGUQAVFUPUKVEUODVEULCNVDGZJZCKUOCV
-      BVDUFVKUNCVJUMULUMCVDCVCUGUHQSPTQSPTPUI $.
+      wceq albii exbii csn cab df-1c eqeq2i eqabb dfcleq df-sn eqabri mpbir ) E
+      FGZABHZCAHZCDIZJZCKZDLZJZAKZBLZBADCMUJBNZERZBLUSBEOVAURBVAUKANZDNZUAZRZDL
+      ZJZAKZURVAUTVFAUBZRVHEVIUTADUCUDVFAUTUEPVGUQAVFUPUKVEUODVEULCNVDGZJZCKUOC
+      VBVDUFVKUNCVJUMULUMCVDCVCUGUHQSPTQSPTPUI $.
   $}
 
   $( Equality theorem for unit power class.  (Contributed by SF,
@@ -37383,11 +37383,11 @@ Kuratowski ordered pairs (continued)
     elp6 $p |- ( A e. V -> ( A e. P6 B <-> A. x << x , { A } >> e. B ) ) $=
       ( vy wcel cp6 cvv csn cxpk wss cv copk wal wceq sneq wi vex albii bitri
       sneqd xpkeq2d sseq1d df-p6 elab2g xpkssvvk ssrelk ax-mp opkelxpk biantrur
-      wb wa df-sn eqabi 3bitr2i imbi1i snex opkeq2 eleq1d ceqsalv syl6bb ) BDFB
-      CGZFHBIZIZJZCKZALZVCMZCFZANZHELZIZIZJZCKVFEBVBDVKBOZVNVECVOVMVDHVOVLVCVKB
-      PUAUBUCECUDUEVFVGVKMZVEFZVPCFZQZENZANZVJVEHHJKVFWAUKHVDUFAEVECUGUHVTVIAVT
-      VKVCOZVRQZENVIVSWCEVQWBVRVQVGHFZVKVDFZULWEWBVGVKHVDARZERUIWDWEWFUJWBEVDEV
-      CUMUNUOUPSVRVIEVCBUQWBVPVHCVKVCVGURUSUTTSTVA $.
+      wb wa df-sn eqabri 3bitr2i imbi1i snex opkeq2 eleq1d ceqsalv syl6bb ) BDF
+      BCGZFHBIZIZJZCKZALZVCMZCFZANZHELZIZIZJZCKVFEBVBDVKBOZVNVECVOVMVDHVOVLVCVK
+      BPUAUBUCECUDUEVFVGVKMZVEFZVPCFZQZENZANZVJVEHHJKVFWAUKHVDUFAEVECUGUHVTVIAV
+      TVKVCOZVRQZENVIVSWCEVQWBVRVQVGHFZVKVDFZULWEWBVGVKHVDARZERUIWDWEWFUJWBEVDE
+      VCUMUNUOUPSVRVIEVCBUQWBVPVHCVKVCVGURUSUTTSTVA $.
   $}
 
   ${
@@ -38093,11 +38093,11 @@ Kuratowski ordered pairs (continued)
        SF, 20-Jan-2015.) $)
     unipw1 $p |- U. ~P1 A = A $=
       ( vx vy vz cpw1 cuni cv wcel wel wa wex csn wceq eluni elpw1 anbi1i ancom
-      wrex weq 3bitri r19.41v exbii risset snex eleq2 df-sn eqabi equcom rexbii
-      3bitr4i ceqsexv rexcom4 3bitr2ri eqriv ) BAEZFZABGZUPHBCIZCGZUOHZJZCKUSDG
-      ZLZMZURJZDARZCKZUQAHZCUQUONVAVFCUTURJVDDARZURJVAVFUTVIURDUSAOPURUTQVDURDA
-      UAUJUBVHDBSZDARVECKZDARVGDUQAUCVKVJDAVKUQVCHZBDSZVJURVLCVCVBUDUSVCUQUEUKV
-      MBVCBVBUFUGBDUHTUIVEDCAULUMTUN $.
+      wrex weq 3bitri r19.41v 3bitr4i exbii risset ceqsexv eqabri equcom rexbii
+      snex eleq2 df-sn rexcom4 3bitr2ri eqriv ) BAEZFZABGZUPHBCIZCGZUOHZJZCKUSD
+      GZLZMZURJZDARZCKZUQAHZCUQUONVAVFCUTURJVDDARZURJVAVFUTVIURDUSAOPURUTQVDURD
+      AUAUBUCVHDBSZDARVECKZDARVGDUQAUDVKVJDAVKUQVCHZBDSZVJURVLCVCVBUIUSVCUQUJUE
+      VMBVCBVBUKUFBDUGTUHVEDCAULUMTUN $.
   $}
 
   $( Biconditional existence for unit power class.  (Contributed by SF,
@@ -42745,10 +42745,10 @@ Ins3_k SI_k ( ( ~P 1c X._k _V ) \
     phi011lem1 $p |- ( ( Phi A u. { 0c } ) = ( Phi B u. { 0c } ) ->
       Phi A C_ Phi B ) $=
       ( vz cphi c0c csn wceq cv wcel wn ssun1 sseli eleq2 syl5ib 0cnelphi eleq1
-      cun wi mtbiri wo con2i a1i elun df-sn eqabi orbi2i biimpi orcomd ord ee22
-      bitri ssrdv ) ADZEFZQZBDZUNQZGZCUMUPURCHZUMIZUSUQIZUSEGZJZUSUPIZUTUSUOIUR
-      VAUMUOUSUMUNKLUOUQUSMNUTVCRURVBUTVBUTEUMIAOUSEUMPSUAUBVAVBVDVAVDVBVAVDVBT
-      ZVAVDUSUNIZTVEUSUPUNUCVFVBVDVBCUNCEUDUEUFUKUGUHUIUJUL $.
+      cun wi mtbiri wo con2i a1i elun df-sn eqabri orbi2i bitri biimpi ord ee22
+      orcomd ssrdv ) ADZEFZQZBDZUNQZGZCUMUPURCHZUMIZUSUQIZUSEGZJZUSUPIZUTUSUOIU
+      RVAUMUOUSUMUNKLUOUQUSMNUTVCRURVBUTVBUTEUMIAOUSEUMPSUAUBVAVBVDVAVDVBVAVDVB
+      TZVAVDUSUNIZTVEUSUPUNUCVFVBVDVBCUNCEUDUEUFUGUHUKUIUJUL $.
   $}
 
   $( ` ( Phi A u. { 0c } ) ` is one-to-one.  Theorem X.2.4 of [Rosser] p. 282.
@@ -45414,7 +45414,7 @@ We use their notation ("onto" under the arrow).  For alternate
     $( Representation of a constant function using ordered pairs.  (Contributed
        by NM, 12-Oct-1999.) $)
     fconstopab $p |- ( A X. { B } ) = { <. x , y >. | ( x e. A /\ y = B ) } $=
-      ( csn cxp cv wcel wa copab wceq df-xp df-sn eqabi anbi2i opabbii eqtri )
+      ( csn cxp cv wcel wa copab wceq df-xp df-sn eqabri anbi2i opabbii eqtri )
       CDEZFAGCHZBGZRHZIZABJSTDKZIZABJABCRLUBUDABUAUCSUCBRBDMNOPQ $.
   $}
 
@@ -50338,11 +50338,11 @@ singleton of the first member (with no sethood assumptions on ` B ` ).
                   E. x e. B ( F ` x ) = C ) ) $=
       ( vy wfn wss wa cima wcel cv cfv wceq wrex cvv anim2i eleq1 wb wi rexbidv
       elex fvex mpbii rexlimivw eqeq2 bibi12d imbi2d wfun cdm fnfun adantr fndm
-      cab sseq2d biimpar dfimafn syl2anc eqabd vtoclg impcom pm5.21nd ) EBGZCBH
-      ZIZDECJZKZALZEMZDNZACOZVEDPKZIVGVLVEDVFUBQVKVLVEVJVLACVJVIPKVLVHEUCVIDPRU
-      DUEQVLVEVGVKSZVEFLZVFKZVIVNNZACOZSZTVEVMTFDPVNDNZVRVMVEVSVOVGVQVKVNDVFRVS
-      VPVJACVNDVIUFUAUGUHVEVQFVFVEEUIZCEUJZHZVFVQFUNNVCVTVDBEUKULVCWBVDVCWABCBE
-      UMUOUPAFCEUQURUSUTVAVB $.
+      cab sseq2d biimpar dfimafn syl2anc eqabrd vtoclg impcom pm5.21nd ) EBGZCB
+      HZIZDECJZKZALZEMZDNZACOZVEDPKZIVGVLVEDVFUBQVKVLVEVJVLACVJVIPKVLVHEUCVIDPR
+      UDUEQVLVEVGVKSZVEFLZVFKZVIVNNZACOZSZTVEVMTFDPVNDNZVRVMVEVSVOVGVQVKVNDVFRV
+      SVPVJACVNDVIUFUAUGUHVEVQFVFVEEUIZCEUJZHZVFVQFUNNVCVTVDBEUKULVCWBVDVCWABCB
+      EUMUOUPAFCEUQURUSUTVAVB $.
   $}
 
   $( Membership in the preimage of a singleton, under a function.  (Contributed
@@ -55974,16 +55974,16 @@ result of an operator (deduction version).  (Contributed by Paul
        9-Mar-2015.) $)
     fvfullfunlem3 $p |- ( A e. dom ( ( _I o. F ) \ ( ~ _I o. F ) ) ->
        ( ( ( _I o. F ) \ ( ~ _I o. F ) ) ` A ) = ( F ` A ) ) $=
-      ( vx vy vz cid ccom wcel cfv wss wceq cv wbr wa brres fvfullfunlem1 eqabi
-      wal weu cvv ccompl cdif cdm cres wfun weq wi dffun2 anbi2i bitri tz6.12-1
-      adantrl adantl eqtr3d adantlr syl2anb mpgbir cxp cin fvfullfunlem2 ssdmrn
-      gen2 crn xpss2 ax-mp sstri ssini df-res sseqtr4i funssfv mp3an12 fvres
-      ssv ) AFBGFUABGUBZUCZHZABVOUDZIZAVNIZABIVQUEZVNVQJVPVRVSKVTCLZDLZVQMZWAEL
-      ZVQMZNDEUFZUGZERDRCCDEVQUHWGDEWCWAWBBMZWAWDBMZESZNZWIWHDSZNZWFWEWCWHWAVOH
-      ZNWKWAWBBVOOWNWJWHWJCVOCEBPQUIUJWEWIWNNWMWAWDBVOOWNWLWIWLCVOCDBPQUIUJWHWM
-      WFWJWHWMNWABIZWBWDWHWLWOWBKWIDWAWBBUKULWMWOWDKWHDWAWDBUKUMUNUOUPVBUQVNBVO
-      TURZUSVQVNBWPBUTVNVOVNVCZURZWPVNVAWQTJWRWPJWQVMWQTVOVDVEVFVGBVOVHVIAVQVNV
-      JVKAVOBVLUN $.
+      ( vx vy vz cid ccom wcel cfv wss wceq cv wbr wal weu fvfullfunlem1 eqabri
+      wa brres cvv ccompl cdif cdm cres wfun weq wi dffun2 anbi2i bitri adantrl
+      tz6.12-1 adantl eqtr3d adantlr syl2anb gen2 cxp cin fvfullfunlem2 crn ssv
+      mpgbir ssdmrn xpss2 ax-mp sstri ssini df-res sseqtr4i funssfv mp3an12
+      fvres ) AFBGFUABGUBZUCZHZABVOUDZIZAVNIZABIVQUEZVNVQJVPVRVSKVTCLZDLZVQMZWA
+      ELZVQMZRDEUFZUGZENDNCCDEVQUHWGDEWCWAWBBMZWAWDBMZEOZRZWIWHDOZRZWFWEWCWHWAV
+      OHZRWKWAWBBVOSWNWJWHWJCVOCEBPQUIUJWEWIWNRWMWAWDBVOSWNWLWIWLCVOCDBPQUIUJWH
+      WMWFWJWHWMRWABIZWBWDWHWLWOWBKWIDWAWBBULUKWMWOWDKWHDWAWDBULUMUNUOUPUQVCVNB
+      VOTURZUSVQVNBWPBUTVNVOVNVAZURZWPVNVDWQTJWRWPJWQVBWQTVOVEVFVGVHBVOVIVJAVQV
+      NVKVLAVOBVMUN $.
   $}
 
   ${
@@ -55994,13 +55994,13 @@ result of an operator (deduction version).  (Contributed by Paul
       ( vx vy cvv wcel cfv wceq cv fveq2 cid ccom ccompl c0 wfn wa mp3an12 mpan
       0ex eqtr4d cfullfun eqeq12d cdm csn cxp cun df-fullfun fveq1i cin incompl
       cdif wfun fnfullfunlem2 funfn fnconstg ax-mp fvun1 fvfullfunlem3 eqtrd wn
-      mpbi vex elcompl fvun2 sylbir wbr weu fvfullfunlem1 eqabi tz6.12-2 sylnbi
-      fvconst2 pm2.61i eqtri vtoclg fvprc ) AEFZABUAZGZABGZHZCIZVRGZWBBGZHWACAE
-      WBAHWCVSWDVTWBAVRJWBABJUBWCWBKBLKMBLUKZWEUCZMZNUDUEZUFZGZWDWBVRWIBUGUHWBW
-      FFZWJWDHWKWJWBWEGZWDWFWGUINHZWKWJWLHZWFUJZWEWFOZWHWGOZWMWKPWNWEULWPBUMWEU
-      NVAZNEFWQSWGNEUOUPZWFWGWEWHWBUQQRWBBURUSWKUTZWJWBWHGZWDWTWBWGFZWJXAHZWBWF
-      CVBVCZWMXBXCWOWPWQWMXBPXCWRWSWFWGWEWHWBVDQRVEWTWDNXAWKWBDIBVFDVGZWDNHXECW
-      FCDBVHVIDWBBVJVKWTXBXANHXDWGNWBSVLVETTVMVNVOVQUTVSNVTAVRVPABVPTVM $.
+      mpbi vex elcompl sylbir wbr fvfullfunlem1 eqabri tz6.12-2 sylnbi fvconst2
+      fvun2 weu pm2.61i eqtri vtoclg fvprc ) AEFZABUAZGZABGZHZCIZVRGZWBBGZHWACA
+      EWBAHWCVSWDVTWBAVRJWBABJUBWCWBKBLKMBLUKZWEUCZMZNUDUEZUFZGZWDWBVRWIBUGUHWB
+      WFFZWJWDHWKWJWBWEGZWDWFWGUINHZWKWJWLHZWFUJZWEWFOZWHWGOZWMWKPWNWEULWPBUMWE
+      UNVAZNEFWQSWGNEUOUPZWFWGWEWHWBUQQRWBBURUSWKUTZWJWBWHGZWDWTWBWGFZWJXAHZWBW
+      FCVBVCZWMXBXCWOWPWQWMXBPXCWRWSWFWGWEWHWBVKQRVDWTWDNXAWKWBDIBVEDVLZWDNHXEC
+      WFCDBVFVGDWBBVHVIWTXBXANHXDWGNWBSVJVDTTVMVNVOVQUTVSNVTAVRVPABVPTVM $.
   $}
 
   $( Binary relationship of the full function operation.  (Contributed by SF,
@@ -57814,12 +57814,12 @@ the first case of his notation (simple exponentiation) and subscript it
     pmvalg $p |- ( ( A e. C /\ B e. D ) ->
                   ( A ^pm B ) = { f e. ~P ( B X. A ) | Fun f } ) $=
       ( vx vy wcel cvv cpm cv cxp cpw crab wceq elex wa cab pweqd biidd co wfun
-      wss df-rab ancom df-pw eqabi anbi2i bitri abbii eqtri pmex syl5eqel xpeq2
-      ancoms rabeqbidv xpeq1 df-pm ovmpt2g mpd3an3 syl2an ) ACHAIHZBIHZABJUAEKZ
-      UBZEBALZMZNZOZBDHACPBDPVBVCVHIHVIVBVCQVHVEVDVFUCZQZERZIVHVDVGHZVEQZERVLVE
-      EVGUDVNVKEVNVEVMQVKVMVEUEVMVJVEVJEVGEVFUFUGUHUIUJUKVCVBVLIHBAIIEULUOUMFGA
-      BIIVEEGKZFKZLZMZNVHJVEEVOALZMZNIVPAOZVEVEEVRVTWAVQVSVPAVOUNSWAVETUPVOBOZV
-      EVEEVTVGWBVSVFVOBAUQSWBVETUPFGEURUSUTVA $.
+      wss df-rab ancom df-pw eqabri anbi2i bitri abbii eqtri syl5eqel rabeqbidv
+      pmex ancoms xpeq2 xpeq1 df-pm ovmpt2g mpd3an3 syl2an ) ACHAIHZBIHZABJUAEK
+      ZUBZEBALZMZNZOZBDHACPBDPVBVCVHIHVIVBVCQVHVEVDVFUCZQZERZIVHVDVGHZVEQZERVLV
+      EEVGUDVNVKEVNVEVMQVKVMVEUEVMVJVEVJEVGEVFUFUGUHUIUJUKVCVBVLIHBAIIEUNUOULFG
+      ABIIVEEGKZFKZLZMZNVHJVEEVOALZMZNIVPAOZVEVEEVRVTWAVQVSVPAVOUPSWAVETUMVOBOZ
+      VEVEEVTVGWBVSVFVOBAUQSWBVETUMFGEURUSUTVA $.
   $}
 
   ${
@@ -58718,15 +58718,15 @@ the first case of his notation (simple exponentiation) and subscript it
     enpw1pw $p |- ~P1 ~P A ~~ ~P ~P1 A $=
       ( vy vx vz cpw cpw1 cpw1fn wf1o wbr c1c wss ax-mp wceq cv wrex wa wex vex
       wcel cres cen cima wf1 pw1fnf1o f1of1 pw1ss1c f1ores mp2an wb df-ima elpw
-      cab sspw1 df-rex df-pw eqabi anbi1i exbii bitr2i 3bitri csn elpw1 r19.41v
-      bitr4i rexcom4 snex breq1 ceqsexv brpw1fn bitri rexbii bitr3i abbi2i mpbi
-      eqtr4i f1oeq3 pw1fnex pwex pw1ex resex f1oen ) AFZGZAGZFZHWDUAZIZWDWFUBJW
-      DHWDUCZWGIZWHKKFZHUDZWDKLWJKWKHIWLUEKWKHUFMWCUGKWKWDHUHUIWIWFNWJWHUJWICOZ
-      DOZHJZCWDPZDUMWFDCHWDUKWPDWFWNWFTZWNEOZGNZEWCPZWPWQWNWELWRALZWSQZERZWTWNW
-      EDSZULEWNAXDUNWTWRWCTZWSQZERXCWSEWCUOXFXBEXEXAWSXAEWCEAUPUQURUSUTVAWPWMWD
-      TZWOQZCRWMWRVBZNZWOQZEWCPZCRZWTWOCWDUOXHXLCXHXJEWCPZWOQXLXGXNWOEWMWCVCURX
-      JWOEWCVDVEUSXMXKCRZEWCPWTXKECWCVFXOWSEWCXOXIWNHJZWSWOXPCXIWRVGWMXIWNHVHVI
-      WRWNESVJVKVLVMVAVEVNVPWIWFWDWGVQMVOWDWFWGHWDVRWCABVSVTWAWBM $.
+      cab sspw1 df-rex df-pw eqabri anbi1i exbii bitr2i 3bitri csn elpw1 bitr4i
+      r19.41v rexcom4 snex breq1 ceqsexv bitri rexbii bitr3i abbi2i eqtr4i mpbi
+      brpw1fn f1oeq3 pw1fnex pwex pw1ex resex f1oen ) AFZGZAGZFZHWDUAZIZWDWFUBJ
+      WDHWDUCZWGIZWHKKFZHUDZWDKLWJKWKHIWLUEKWKHUFMWCUGKWKWDHUHUIWIWFNWJWHUJWICO
+      ZDOZHJZCWDPZDUMWFDCHWDUKWPDWFWNWFTZWNEOZGNZEWCPZWPWQWNWELWRALZWSQZERZWTWN
+      WEDSZULEWNAXDUNWTWRWCTZWSQZERXCWSEWCUOXFXBEXEXAWSXAEWCEAUPUQURUSUTVAWPWMW
+      DTZWOQZCRWMWRVBZNZWOQZEWCPZCRZWTWOCWDUOXHXLCXHXJEWCPZWOQXLXGXNWOEWMWCVCUR
+      XJWOEWCVEVDUSXMXKCRZEWCPWTXKECWCVFXOWSEWCXOXIWNHJZWSWOXPCXIWRVGWMXIWNHVHV
+      IWRWNESVPVJVKVLVAVDVMVNWIWFWDWGVQMVOWDWFWGHWDVRWCABVSVTWAWBM $.
   $}
 
   ${