diff --git a/changes-set.txt b/changes-set.txt
index ca2e872dab..d6cc7ed93f 100644
--- a/changes-set.txt
+++ b/changes-set.txt
@@ -93,6 +93,8 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+19-Dec-24 3albii    [same]      moved from PM's mathbox to main set.mm
+19-Dec-24 ssrel3    [same]      moved from PM's mathbox to main set.mm
 17-Dec-24 ffvelrnd  ffvelcdmd
 17-Dec-24 ffvelrnda ffvelcdmda
 17-Dec-24 ffvelrni  ffvelcdmi
diff --git a/discouraged b/discouraged
index 493db8fc95..d4fb32707c 100644
--- a/discouraged
+++ b/discouraged
@@ -15793,6 +15793,7 @@ New usage of "conventions-comments" is discouraged (0 uses).
 New usage of "conventions-labels" is discouraged (0 uses).
 New usage of "copsex2gOLD" is discouraged (0 uses).
 New usage of "copsexg" is discouraged (1 uses).
+New usage of "cotrgOLD" is discouraged (0 uses).
 New usage of "counop" is discouraged (0 uses).
 New usage of "crhmsubcALTV" is discouraged (1 uses).
 New usage of "cringcALTV" is discouraged (9 uses).
@@ -16032,6 +16033,8 @@ New usage of "dfcnqs" is discouraged (4 uses).
 New usage of "dfeu" is discouraged (0 uses).
 New usage of "dffr2ALT" is discouraged (0 uses).
 New usage of "dffun2OLD" is discouraged (0 uses).
+New usage of "dffun3OLD" is discouraged (0 uses).
+New usage of "dffun6OLD" is discouraged (0 uses).
 New usage of "dfhnorm2" is discouraged (3 uses).
 New usage of "dfid2" is discouraged (1 uses).
 New usage of "dfid2OLD" is discouraged (0 uses).
@@ -16108,6 +16111,7 @@ New usage of "dicfnN" is discouraged (1 uses).
 New usage of "dicvalrelN" is discouraged (0 uses).
 New usage of "dif1enALT" is discouraged (0 uses).
 New usage of "difidALT" is discouraged (0 uses).
+New usage of "difopabOLD" is discouraged (0 uses).
 New usage of "dih0bN" is discouraged (0 uses).
 New usage of "dih0vbN" is discouraged (0 uses).
 New usage of "dih2dimbALTN" is discouraged (0 uses).
@@ -16729,6 +16733,8 @@ New usage of "funcringcsetclem8ALTV" is discouraged (1 uses).
 New usage of "funcringcsetclem9ALTV" is discouraged (1 uses).
 New usage of "funcrngcsetcALT" is discouraged (0 uses).
 New usage of "fundcmpsurinjALT" is discouraged (0 uses).
+New usage of "funimaexgOLD" is discouraged (0 uses).
+New usage of "funmoOLD" is discouraged (0 uses).
 New usage of "funop" is discouraged (2 uses).
 New usage of "funopg" is discouraged (0 uses).
 New usage of "funopsn" is discouraged (2 uses).
@@ -17381,6 +17387,7 @@ New usage of "ipval3" is discouraged (1 uses).
 New usage of "ipz" is discouraged (1 uses).
 New usage of "isablo" is discouraged (3 uses).
 New usage of "isabloi" is discouraged (3 uses).
+New usage of "isarep1OLD" is discouraged (0 uses).
 New usage of "isass" is discouraged (1 uses).
 New usage of "isblo" is discouraged (5 uses).
 New usage of "isblo2" is discouraged (1 uses).
@@ -20097,6 +20104,7 @@ Proof modification of "conventions" is discouraged (1 steps).
 Proof modification of "conventions-comments" is discouraged (1 steps).
 Proof modification of "conventions-labels" is discouraged (1 steps).
 Proof modification of "copsex2gOLD" is discouraged (119 steps).
+Proof modification of "cotrgOLD" is discouraged (110 steps).
 Proof modification of "csbcnvgALT" is discouraged (112 steps).
 Proof modification of "csbconstgOLD" is discouraged (8 steps).
 Proof modification of "csbeq2gVD" is discouraged (61 steps).
@@ -20125,6 +20133,8 @@ Proof modification of "dfbi1ALT" is discouraged (100 steps).
 Proof modification of "dfeu" is discouraged (35 steps).
 Proof modification of "dffr2ALT" is discouraged (64 steps).
 Proof modification of "dffun2OLD" is discouraged (157 steps).
+Proof modification of "dffun3OLD" is discouraged (72 steps).
+Proof modification of "dffun6OLD" is discouraged (10 steps).
 Proof modification of "dfid2OLD" is discouraged (3 steps).
 Proof modification of "dfiun2gOLD" is discouraged (131 steps).
 Proof modification of "dfmo" is discouraged (44 steps).
@@ -20155,6 +20165,7 @@ Proof modification of "dfvd3ir" is discouraged (19 steps).
 Proof modification of "dfwrecsOLD" is discouraged (619 steps).
 Proof modification of "dif1enALT" is discouraged (335 steps).
 Proof modification of "difidALT" is discouraged (14 steps).
+Proof modification of "difopabOLD" is discouraged (171 steps).
 Proof modification of "dih2dimbALTN" is discouraged (450 steps).
 Proof modification of "disjOLD" is discouraged (71 steps).
 Proof modification of "dju1p1e2" is discouraged (72 steps).
@@ -20649,6 +20660,8 @@ Proof modification of "fsplitOLD" is discouraged (234 steps).
 Proof modification of "fuchomOLD" is discouraged (229 steps).
 Proof modification of "funcrngcsetcALT" is discouraged (765 steps).
 Proof modification of "fundcmpsurinjALT" is discouraged (221 steps).
+Proof modification of "funimaexgOLD" is discouraged (133 steps).
+Proof modification of "funmoOLD" is discouraged (115 steps).
 Proof modification of "fvilbdRP" is discouraged (27 steps).
 Proof modification of "fvimacnvALT" is discouraged (102 steps).
 Proof modification of "fvmptopabOLD" is discouraged (185 steps).
@@ -20758,6 +20771,7 @@ Proof modification of "int2" is discouraged (14 steps).
 Proof modification of "int3" is discouraged (17 steps).
 Proof modification of "intprOLD" is discouraged (112 steps).
 Proof modification of "intprgOLD" is discouraged (80 steps).
+Proof modification of "isarep1OLD" is discouraged (106 steps).
 Proof modification of "iscmgmALT" is discouraged (57 steps).
 Proof modification of "iscsgrpALT" is discouraged (57 steps).
 Proof modification of "iseriALT" is discouraged (54 steps).
diff --git a/set.mm b/set.mm
index 518c6b8517..c1f76999f4 100644
--- a/set.mm
+++ b/set.mm
@@ -15008,6 +15008,11 @@ only postulated (that is, axiomatic) rule of inference of predicate
        equivalence.  (Contributed by NM, 9-Mar-1997.) $)
     2albii $p |- ( A. x A. y ph <-> A. x A. y ps ) $=
       ( wal albii ) ADFBDFCABDEGG $.
+
+    $( Inference adding three universal quantifiers to both sides of an
+       equivalence.  (Contributed by Peter Mazsa, 10-Aug-2018.) $)
+    3albii $p |- ( A. x A. y A. z ph <-> A. x A. y A. z ps ) $=
+      ( wal 2albii albii ) AEGDGBEGDGCABDEFHI $.
   $}
 
   $( Closed form of ~ sylg .  (Contributed by BJ, 2-May-2019.) $)
@@ -54655,6 +54660,15 @@ of the restricted converse (see ~ cnvrescnv ).  (Contributed by NM,
       KVAVKVJUTLZMZGPVPGEUTTWEVOGWDVNVKABVJCDULUOUPSGEFTUQURUS $.
   $}
 
+  ${
+    $d A x y $.  $d B x y $.
+    $( Subclass relation in another form when the subclass is a relation.
+       (Contributed by Peter Mazsa, 16-Feb-2019.) $)
+    ssrel3 $p |- ( Rel A -> ( A C_ B <-> A. x A. y ( x A y -> x B y ) ) ) $=
+      ( wrel wss cv cop wcel wi wal wbr ssrel df-br imbi12i 2albii bitr4di ) CE
+      CDFAGZBGZHZCIZTDIZJZBKAKRSCLZRSDLZJZBKAKABCDMUFUCABUDUAUEUBRSCNRSDNOPQ $.
+  $}
+
   ${
     $d x y A $.  $d x y B $.
     relssi.1 $e |- Rel A $.
@@ -55044,9 +55058,21 @@ of the restricted converse (see ~ cnvrescnv ).  (Contributed by NM,
       UICDEFQUDUE $.
 
     $( Difference of two ordered-pair class abstractions.  (Contributed by
-       Stefan O'Rear, 17-Jan-2015.) $)
+       Stefan O'Rear, 17-Jan-2015.)  (Proof shortened by SN, 19-Dec-2024.) $)
     difopab $p |- ( { <. x , y >. | ph } \ { <. x , y >. | ps } ) =
         { <. x , y >. | ( ph /\ -. ps ) } $=
+      ( vz vw copab cdif wn wa wrel relopabv cv wcel wsb sban sbbii vopelopabsb
+      sbn 3bitr4ri reldif ax-mp cop notbii anbi12i eldif 3bitr4i eqrelriiv ) EF
+      ACDGZBCDGZHZABIZJZCDGZUIKUKKACDLUIUJUAUBUMCDLEMFMUCZUINZUOUJNZIZJZUMDFOZC
+      EOZUOUKNUOUNNADFOZULDFOZJZCEOVBCEOZVCCEOZJVAUSVBVCCEPUTVDCEAULDFPQUPVEURV
+      FACDEFRBDFOZIZCEOVGCEOZIVFURVGCESVCVHCEBDFSQUQVIBCDEFRUDTUETUOUIUJUFUMCDE
+      FRUGUH $.
+
+    $( Obsolete version of ~ difopab as of 19-Dec-2024.  (Contributed by Stefan
+       O'Rear, 17-Jan-2015.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    difopabOLD $p |- ( { <. x , y >. | ph } \ { <. x , y >. | ps } ) =
+        { <. x , y >. | ( ph /\ -. ps ) } $=
       ( vz vw copab wn wa wrel relopabv cv wcel wsbc sbcan sbcbii opelopabsb wb
       cvv sbcng cdif reldif ax-mp cop elv notbii 3bitr4ri anbi12i eldif 3bitr4i
       eqrelriiv ) EFACDGZBCDGZUAZABHZIZCDGZULJUNJACDKULUMUBUCUPCDKELZFLZUDZULMZ
@@ -57422,20 +57448,42 @@ the restriction (of the relation) to the singleton containing this
       ( wrel ccnv wbr wb relbrcnvg ax-mp ) CEABCFGBACGHDABCIJ $.
   $}
 
+  ${
+    $d A x y z $.  $d B x y z $.
+    $( A composition is a relation.  Exercise 24 of [TakeutiZaring] p. 25.
+       (Contributed by NM, 26-Jan-1997.) $)
+    relco $p |- Rel ( A o. B ) $=
+      ( vx vz vy cv wbr wa wex ccom df-co relopabiv ) CFDFZBGMEFAGHDICEABJCEDAB
+      KL $.
+  $}
+
   ${
     $d x y z A $.  $d x y z B $.  $d x y z C $.
     $( Two ways of saying that the composition of two relations is included in
        a third relation.  See its special instance ~ cotr for the main
        application.  (Contributed by NM, 27-Dec-1996.)  (Proof shortened by
        Andrew Salmon, 27-Aug-2011.)  Generalized from its special instance
-       ~ cotr .  (Revised by Richard Penner, 24-Dec-2019.) $)
+       ~ cotr .  (Revised by Richard Penner, 24-Dec-2019.)  (Proof shortened by
+       SN, 19-Dec-2024.) $)
     cotrg $p |-
       ( ( A o. B ) C_ C <-> A. x A. y A. z ( ( x B y /\ y A z ) -> x C z ) ) $=
-      ( ccom wss cv cop wcel wi wal wbr wa wrel wb vex albii bitri df-co opelco
-      wex relopabiv ssrel ax-mp df-br bicomi imbi12i 19.23v bitr4i alcom ) DEGZ
-      FHZAIZCIZJZUMKZUQFKZLZCMZAMZUOBIZENVCUPDNOZUOUPFNZLZCMBMZAMUMPUNVBQVDBUCZ
-      ACUMACBDEUAUDACUMFUEUFVAVGAVAVFBMZCMVGUTVICUTVHVELVIURVHUSVEBUOUPDEARCRUB
-      VEUSUOUPFUGUHUIVDVEBUJUKSVFCBULTST $.
+      ( ccom wss cv wbr wi wal wa wrel wb relco ssrel3 vex albii bitri wex brco
+      ax-mp imbi1i 19.23v bitr4i alcom ) DEGZFHZAIZCIZUHJZUJUKFJZKZCLZALZUJBIZE
+      JUQUKDJMZUMKZCLBLZALUHNUIUPODEPACUHFQUCUOUTAUOUSBLZCLUTUNVACUNURBUAZUMKVA
+      ULVBUMBUJUKDEARCRUBUDURUMBUEUFSUSCBUGTST $.
+
+    $( Obsolete version of ~ cotrg as of 19-Dec-2024.  (Contributed by NM,
+       27-Dec-1996.)  (Proof shortened by Andrew Salmon, 27-Aug-2011.)
+       Generalized from its special instance ~ cotr .  (Revised by Richard
+       Penner, 24-Dec-2019.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    cotrgOLD $p |-
+      ( ( A o. B ) C_ C <-> A. x A. y A. z ( ( x B y /\ y A z ) -> x C z ) ) $=
+      ( ccom wss cv cop wcel wi wal wbr wa wrel wb vex albii bitri relco opelco
+      ssrel ax-mp wex df-br bicomi imbi12i 19.23v bitr4i alcom ) DEGZFHZAIZCIZJ
+      ZULKZUPFKZLZCMZAMZUNBIZENVBUODNOZUNUOFNZLZCMBMZAMULPUMVAQDEUAACULFUCUDUTV
+      FAUTVEBMZCMVFUSVGCUSVCBUEZVDLVGUQVHURVDBUNUODEARCRUBVDURUNUOFUFUGUHVCVDBU
+      IUJSVECBUKTST $.
   $}
 
   ${
@@ -58606,12 +58654,6 @@ singleton of the first member (with no sethood assumptions on ` B ` ).
 
   ${
     $d w x y z A $.  $d w x y z B $.  $d w x y z C $.
-    $( A composition is a relation.  Exercise 24 of [TakeutiZaring] p. 25.
-       (Contributed by NM, 26-Jan-1997.) $)
-    relco $p |- Rel ( A o. B ) $=
-      ( vx vz vy cv wbr wa wex ccom df-co relopabiv ) CFDFZBGMEFAGHDICEABJCEDAB
-      KL $.
-
     $( Alternate definition of a class composition, using only one bound
        variable.  (Contributed by NM, 19-Dec-2008.) $)
     dfco2 $p |- ( A o. B )
@@ -61362,16 +61404,13 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ).
   ${
     $d A x y z $.
     $( Alternate definition of a function.  (Contributed by NM, 29-Dec-1996.)
-       Avoid ~ ax-10 , ~ ax-12 .  (Revised by SN, 11-Nov-2024.) $)
+       Avoid ~ ax-10 , ~ ax-12 .  (Revised by SN, 19-Dec-2024.) $)
     dffun2 $p |- ( Fun A <-> ( Rel A /\
                  A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) ) ) $=
-      ( wfun wrel ccnv ccom cid wss wa cv wbr wi wal wcel wex vex bitri 2albii
-      wceq df-fun cop wb relco ssrel ax-mp opelco brcnv anbi1i exbii df-br ideq
-      bitr3i imbi12i alrot3 19.23v bitr2i 3bitri anbi2i ) DEDFZDDGZHZIJZKVAALZB
-      LZDMZVECLZDMZKZVFVHUAZNZCOBOAOZKDUBVDVMVAVDVFVHUCZVCPZVNIPZNZCOBOZVJAQZVK
-      NZCOBOZVMVCFVDVRUDDVBUEBCVCIUFUGVQVTBCVOVSVPVKVOVFVEVBMZVIKZAQVSAVFVHDVBB
-      RZCRZUHWCVJAWBVGVIVFVEDWDARUIUJUKSVPVFVHIMVKVFVHIULVFVHWEUMUNUOTVMVLAOZCO
-      BOWAVLABCUPWFVTBCVJVKAUQTURUSUTS $.
+      ( wfun wrel ccnv ccom cid wss wa cv wbr weq wi wal df-fun cotrg vex bitri
+      alcom brcnv anbi1i ideq imbi12i 3albii anbi2i ) DEDFZDDGZHIJZKUHALZBLZDMZ
+      UKCLZDMZKZBCNZOZCPBPAPZKDQUJUSUHUJULUKUIMZUOKZULUNIMZOZCPZAPBPZUSBACDUIIR
+      VEVDBPAPUSVDBAUAVCURABCVAUPVBUQUTUMUOULUKDBSASUBUCULUNCSUDUEUFTTUGT $.
     $( $j usage 'dffun2' avoids 'ax-10' 'ax-12'; $)
 
     $( Obsolete version of ~ dffun2 as of 11-Dec-2024.  (Contributed by NM,
@@ -61385,10 +61424,34 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ).
       CUBZTZCLZBLALZIDUCUTVIUQUTVBVAURKZVDIZAMZVFTZCLZBLZVHALZBLVIUTUSVFBCNZHVL
       BCNZVQHVOGVQUSBCUDUEUSVRVQBCADURUFUGVLVFBCUHOVNVPBVNVGALZCLVPVMVSCVMVEAMZ
       VFTVSVLVTVFVKVEAVJVCVDVBVADBPAPUIUJUKUMVEVFAUNUOQVGCARSQVHBAROUPS $.
+  $}
 
-    $( Alternate definition of function.  (Contributed by NM, 29-Dec-1996.) $)
+  ${
+    $d F x y z $.
+    $( Alternate definition of a function using "at most one" notation.
+       (Contributed by NM, 9-Mar-1995.)  Avoid ~ ax-10 , ~ ax-12 .  (Revised by
+       SN, 19-Dec-2024.) $)
+    dffun6 $p |- ( Fun F <-> ( Rel F /\ A. x E* y x F y ) ) $=
+      ( vz wfun wrel cv wbr wa weq wal wmo dffun2 breq2 mo4 albii anbi2i bitr4i
+      wi ) CECFZAGZBGZCHZUADGZCHZIBDJSDKBKZAKZITUCBLZAKZIABDCMUIUGTUHUFAUCUEBDU
+      BUDUACNOPQR $.
+    $( $j usage 'dffun6' avoids 'ax-10' 'ax-12'; $)
+  $}
+
+  ${
+    $d A x y z $.
+    $( Alternate definition of function.  (Contributed by NM, 29-Dec-1996.)
+       (Proof shortened by SN, 19-Dec-2024.) $)
     dffun3 $p |- ( Fun A <-> ( Rel A /\
                  A. x E. z A. y ( x A y -> y = z ) ) ) $=
+      ( wfun wrel cv wbr wmo wal wa weq wi wex dffun6 df-mo albii anbi2i bitri
+      ) DEDFZAGBGDHZBIZAJZKTUABCLMBJCNZAJZKABDOUCUETUBUDAUABCPQRS $.
+
+    $( Obsolete version of ~ dffun3 as of 19-Dec-2024.  Alternate definition of
+       function.  (Contributed by NM, 29-Dec-1996.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    dffun3OLD $p |- ( Fun A <-> ( Rel A /\
+                 A. x E. z A. y ( x A y -> y = z ) ) ) $=
       ( wfun wrel cv wbr wa weq wal wex dffun2 wmo breq2 mo4 df-mo bitr3i albii
       wi anbi2i bitri ) DEDFZAGZBGZDHZUDCGZDHZIBCJZTCKBKZAKZIUCUFUITBKCLZAKZIAB
       CDMUKUMUCUJULAUJUFBNULUFUHBCUEUGUDDOPUFBCQRSUAUB $.
@@ -61428,14 +61491,26 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ).
 
   ${
     $d x y A $.  $d x y F $.
-    $( Alternate definition of a function using "at most one" notation.
-       (Contributed by NM, 9-Mar-1995.) $)
-    dffun6 $p |- ( Fun F <-> ( Rel F /\ A. x E* y x F y ) ) $=
+    $( Obsolete version of ~ dffun6 as of 19-Dec-2024.  (Contributed by NM,
+       9-Mar-1995.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    dffun6OLD $p |- ( Fun F <-> ( Rel F /\ A. x E* y x F y ) ) $=
       ( nfcv dffun6f ) ABCACDBCDE $.
 
     $( A function has at most one value for each argument.  (Contributed by NM,
-       24-May-1998.) $)
+       24-May-1998.)  (Proof shortened by SN, 19-Dec-2024.) $)
     funmo $p |- ( Fun F -> E* y A F y ) $=
+      ( vx wfun cv wbr cvv wcel wa wi wal wrel dffun6 simplbi brrelex1 ex ancrd
+      wmo syl alrimiv simprbi wceq breq1 mobidv spcgv syl5com moanimv moim sylc
+      sylibr ) CEZBAFZCGZBHIZUNJZKZALUPASZUNASZULUQAULUNUOULCMZUNUOKULUTDFZUMCG
+      ZASZDLZDACNZOUTUNUOBUMCPQTRUAULUOUSKURULVDUOUSULUTVDVEUBVCUSDBHVABUCVBUNA
+      VABUMCUDUEUFUGUOUNAUHUKUNUPAUIUJ $.
+    $( $j usage 'funmo' avoids 'ax-12'; $)
+
+    $( Obsolete version of ~ funmo as of 19-Dec-2024.  (Contributed by NM,
+       24-May-1998.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    funmoOLD $p |- ( Fun F -> E* y A F y ) $=
       ( vx wfun cv wbr cvv wcel wa wi wal wrel dffun6 simplbi brrelex1 ex ancrd
       wmo syl alrimiv breq1 mobidv imbi2d simprbi 19.21bi vtoclg moanimv sylibr
       wceq com12 moim sylc ) CEZBAFZCGZBHIZUPJZKZALURASZUPASZUNUSAUNUPUQUNCMZUP
@@ -62152,11 +62227,24 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ).
     CAABFZFZGZCAGZSCBGZFZFZCABHZGSTHORSCPGZFUBAPCIOUDUASABCIJKUCQCABLMSTLN $.
 
   ${
-    $d w B $.  $d x y z w A $.
+    $d A x y $.  $d B x y $.
     $( Axiom of Replacement using abbreviations.  Axiom 39(vi) of [Quine]
        p. 284.  Compare Exercise 9 of [TakeutiZaring] p. 29.  (Contributed by
-       NM, 10-Sep-2006.) $)
+       NM, 10-Sep-2006.)  Shorten proof and avoid ~ ax-10 , ~ ax-12 .  (Revised
+       by SN, 19-Dec-2024.) $)
     funimaexg $p |- ( ( Fun A /\ B e. C ) -> ( A " B ) e. _V ) $=
+      ( vx vy wcel wfun cima cvv cv wbr wmo wal wrel dffun6 simprbi wa wrex cab
+      dfima2 axrep6g eqeltrid sylan2 ancoms ) BCFZAGZABHZIFZUFUEDJEJAKZELDMZUHU
+      FANUJDEAOPUEUJQUGUIDBRESIDEABTUIDEBCUAUBUCUD $.
+    $( $j usage 'funimaexg' avoids 'ax-10' 'ax-12'; $)
+  $}
+
+  ${
+    $d w B $.  $d x y z w A $.
+    $( Obsolete version of ~ funimaexg as of 19-Dec-2024.  (Contributed by NM,
+       10-Sep-2006.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    funimaexgOLD $p |- ( ( Fun A /\ B e. C ) -> ( A " B ) e. _V ) $=
       ( vw vx vy vz wcel wfun cima cvv cv wceq imaeq2 eleq1d wal wex wel bitri
       wi imbi2d cop dffun5 wa wb nfv axrep4 isset cab dfima3 eqeq2i abeq2 exbii
       wrel sylibr simplbiim vtoclg impcom ) BCHAIZABJZKHZUSADLZJZKHZTUSVATDBCVB
@@ -62183,9 +62271,19 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ).
        If so, we can prove Isabelle's "Axiom of Replacement" conclusion without
        using the Axiom of Replacement, for which I (N. Megill) currently have
        no explanation.  (Contributed by NM, 26-Oct-2006.)  (Proof shortened by
-       Mario Carneiro, 4-Dec-2016.) $)
+       Mario Carneiro, 4-Dec-2016.)  (Proof shortened by SN, 19-Dec-2024.) $)
     isarep1 $p |- ( b e. ( { <. x , y >. | ph } " A ) <->
                  E. x e. A [ b / y ] ph ) $=
+      ( vz cv copab cima wcel wbr wrex wsb elima df-br vopelopabsb bitri rexbii
+      vex cop nfs1v nfv sbequ12r cbvrexw 3bitri ) EGZABCHZDIJFGZUFUGKZFDLACEMZB
+      FMZFDLUJBDLFUFUGDESNUIUKFDUIUHUFTUGJUKUHUFUGOABCFEPQRUKUJFBDUJBFUAUJFUBUJ
+      FBUCUDUE $.
+
+    $( Obsolete version of ~ isarep1 as of 19-Dec-2024.  (Contributed by NM,
+       26-Oct-2006.)  (Proof shortened by Mario Carneiro, 4-Dec-2016.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    isarep1OLD $p |- ( b e. ( { <. x , y >. | ph } " A ) <->
+                 E. x e. A [ b / y ] ph ) $=
       ( vz copab cima wcel wbr wrex wsb vex elima cop wsbc df-br sbsbc 3bitri
       cv opelopabsb sbbii bitr2i rexbii nfs1v nfv sbequ12r cbvrexw ) ETZABCGZDH
       IFTZUIUJJZFDKACELZBFLZFDKUMBDKFUIUJDEMNULUNFDULUKUIOUJIACUIPZBUKPZUNUKUIU
@@ -580559,14 +580657,6 @@ A collection of theorems for commuting equalities (or
   nexmo1 $p |- ( -. E. x ph -> E* x ph ) $=
     ( wex wn weu wi wmo pm2.21 moeu sylibr ) ABCZDKABEZFABGKLHABIJ $.
 
-  ${
-    3albii.1 $e |- ( ph <-> ps ) $.
-    $( Inference adding three universal quantifiers to both sides of an
-       equivalence.  (Contributed by Peter Mazsa, 10-Aug-2018.) $)
-    3albii $p |- ( A. x A. y A. z ph <-> A. x A. y A. z ps ) $=
-      ( wal 2albii albii ) AEGDGBEGDGCABDEFHI $.
-  $}
-
   ${
     3ralbii.1 $e |- ( ph <-> ps ) $.
     $( Inference adding three restricted universal quantifiers to both sides of
@@ -580985,15 +581075,6 @@ A collection of theorems for commuting equalities (or
       AUCNORPQS $.
   $}
 
-  ${
-    $d A x y $.  $d B x y $.
-    $( Subclass relation in another form when the subclass is a relation.
-       (Contributed by Peter Mazsa, 16-Feb-2019.) $)
-    ssrel3 $p |- ( Rel A -> ( A C_ B <-> A. x A. y ( x A y -> x B y ) ) ) $=
-      ( wrel wss cv cop wcel wi wal wbr ssrel df-br imbi12i 2albii bitr4di ) CE
-      CDFAGZBGZHZCIZTDIZJZBKAKRSCLZRSDLZJZBKAKABCDMUFUCABUDUAUEUBRSCNRSDNOPQ $.
-  $}
-
   ${
     $d A x y $.  $d B x y $.
     $( Equality of relations.  (Contributed by Peter Mazsa, 8-Mar-2019.) $)
@@ -750121,18 +750202,30 @@ its dimensional volume (the product of its length in each dimension,
       UNUTBCUOUPTUQ $.
   $}
 
+  ${
+    pimltpnff.1 $e |- F/ x ph $.
+    pimltpnff.2 $e |- F/_ x A $.
+    pimltpnff.3 $e |- ( ( ph /\ x e. A ) -> B e. RR ) $.
+    $( Given a real-valued function, the preimage of an open interval,
+       unbounded below, with upper bound ` +oo ` , is the whole domain.
+       (Contributed by Glauco Siliprandi, 20-Dec-2024.) $)
+    pimltpnff $p |- ( ph -> { x e. A | B < +oo } = A ) $=
+      ( cpnf clt wbr crab wss ssrab2f a1i cv wcel wral wa simpr sylibr cr ltpnf
+      syl jca rabid ex ralrimi nfrab1 dfss3f eqssd ) ADHIJZBCKZCULCLAUKBCFMNABO
+      ZULPZBCQCULLAUNBCEAUMCPZUNAUORZUOUKRUNUPUOUKAUOSUPDUAPUKGDUBUCUDUKBCUETUF
+      UGBCULFUKBCUHUITUJ $.
+  $}
+
   ${
     $d A x $.
     pimltpnf.1 $e |- F/ x ph $.
     pimltpnf.2 $e |- ( ( ph /\ x e. A ) -> B e. RR ) $.
     $( Given a real-valued function, the preimage of an open interval,
        unbounded below, with upper bound ` +oo ` , is the whole domain.
-       (Contributed by Glauco Siliprandi, 26-Jun-2021.) $)
+       (Contributed by Glauco Siliprandi, 26-Jun-2021.)  (Revised by Glauco
+       Siliprandi, 20-Dec-2024.) $)
     pimltpnf $p |- ( ph -> { x e. A | B < +oo } = A ) $=
-      ( cpnf clt wbr crab wss ssrab2 a1i cv wcel wral wa simpr cr sylibr syl ex
-      ltpnf jca rabid ralrimi nfcv nfrab1 dfss3f eqssd ) ADGHIZBCJZCULCKAUKBCLM
-      ABNZULOZBCPCULKAUNBCEAUMCOZUNAUOQZUOUKQUNUPUOUKAUORUPDSOUKFDUCUAUDUKBCUET
-      UBUFBCULBCUGUKBCUHUITUJ $.
+      ( nfcv pimltpnff ) ABCDEBCGFH $.
   $}
 
   ${
@@ -750545,17 +750638,30 @@ its dimensional volume (the product of its length in each dimension,
       CFLWJWNXJXPYCHUNAXQXIYCIPWKWLTTVNYCWRBCWOSWPWQ $.
   $}
 
+  ${
+    pimgtmnff.1 $e |- F/ x ph $.
+    pimgtmnff.2 $e |- F/_ x A $.
+    pimgtmnff.3 $e |- ( ( ph /\ x e. A ) -> B e. RR ) $.
+    $( Given a real-valued function, the preimage of an open interval,
+       unbounded above, with lower bound ` -oo ` , is the whole domain.
+       (Contributed by Glauco Siliprandi, 20-Dec-2024.) $)
+    pimgtmnff $p |- ( ph -> { x e. A | -oo < B } = A ) $=
+      ( cmnf clt wbr crab wss ssrab2f a1i cv wcel wral wa simpr sylibr cr mnflt
+      syl jca rabid ex ralrimi nfrab1 dfss3f eqssd ) AHDIJZBCKZCULCLAUKBCFMNABO
+      ZULPZBCQCULLAUNBCEAUMCPZUNAUORZUOUKRUNUPUOUKAUOSUPDUAPUKGDUBUCUDUKBCUETUF
+      UGBCULFUKBCUHUITUJ $.
+  $}
+
   ${
     $d A x $.
     pimgtmnf.1 $e |- F/ x ph $.
     pimgtmnf.2 $e |- ( ( ph /\ x e. A ) -> B e. RR ) $.
     $( Given a real-valued function, the preimage of an open interval,
        unbounded above, with lower bound ` -oo ` , is the whole domain.
-       (Contributed by Glauco Siliprandi, 26-Jun-2021.) $)
+       (Contributed by Glauco Siliprandi, 26-Jun-2021.)  (Revised by Glauco
+       Siliprandi, 20-Dec-2024.) $)
     pimgtmnf $p |- ( ph -> { x e. A | -oo < B } = A ) $=
-      ( cmnf clt wbr crab cv cmpt cfv wcel wa cr eqidd fvmpt2d eqcomd breq2d
-      rabbida nfmpt1 eqid fmptdf pimgtmnf2 eqtrd ) AGDHIZBCJGBKZBCDLZMZHIZBCJCA
-      UGUKBCEAUHCNOZDUJGHULUJDABCDUIPAUIQFRSTUAABCUIBCDUBABCDPUIEFUIUCUDUEUF $.
+      ( nfcv pimgtmnff ) ABCDEBCGFH $.
   $}
 
   ${
@@ -751313,6 +751419,29 @@ its dimensional volume (the product of its length in each dimension,
       VNAVIVOVJVPAVHBVCCVMUNAVCCDRVMUOUPVATUQURUSABVCDEFHVCUTVBT $.
   $}
 
+  ${
+    $d A y $.  $d B y $.  $d R x y $.
+    smfpimltxrmptf.x $e |- F/ x ph $.
+    smfpimltxrmptf.1 $e |- F/_ x A $.
+    smfpimltxrmptf.s $e |- ( ph -> S e. SAlg ) $.
+    smfpimltxrmptf.b $e |- ( ( ph /\ x e. A ) -> B e. V ) $.
+    smfpimltxrmptf.f $e |- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) ) $.
+    smfpimltxrmptf.r $e |- ( ph -> R e. RR* ) $.
+    $( Given a function measurable w.r.t. to a sigma-algebra, the preimage of
+       an open interval unbounded below is in the subspace sigma-algebra
+       induced by its domain.  (Contributed by Glauco Siliprandi,
+       20-Dec-2024.) $)
+    smfpimltxrmptf $p |- ( ph -> { x e. A | B < R } e. ( S |`t A ) ) $=
+      ( vy clt wbr crab wcel wceq nfcv crest co cv cmpt cfv cdm nfmpt1 nfdm nfv
+      nffv nfbr fveq2 breq1d cbvrabw a1i smfpimltxr eqeltrd dmmptdf2 rabeqf syl
+      eqid wa simpr fvmpt2f syl2anc rabbida eqidd 3eqtrrd eqcomd oveq2d eleq12d
+      mpbird ) ADEOPZBCQZFCUAUBZRBUCZBCDUDZUEZEOPZBVQUFZQZFVTUAUBZRAWANUCZVQUEZ
+      EOPZNVTQZWBWAWFSAVSWEBNVTBVQBCDUGZUHZNVTTVSNUIBWDEOBWCVQWGBWCTUJBOTBETUKV
+      PWCSVRWDEOVPWCVQULUMUNUOANEVTFVQNVQTJLVTVAMUPUQAVNWAVOWBAWAVSBCQZVNVNAVTC
+      SWAWISABVQCDGHIVQVAKURZVSBVTCWHIUSUTAVSVMBCHAVPCRZVBZVRDEOWLWKDGRVRDSAWKV
+      CKBCDGIVDVEUMVFAVNVGVHACVTFUAAVTCWJVIVJVKVL $.
+  $}
+
   ${
     $d A x y $.  $d B y $.  $d R x y $.
     smfpimltxrmpt.x $e |- F/ x ph $.
@@ -751322,17 +751451,10 @@ its dimensional volume (the product of its length in each dimension,
     smfpimltxrmpt.r $e |- ( ph -> R e. RR* ) $.
     $( Given a function measurable w.r.t. to a sigma-algebra, the preimage of
        an open interval unbounded below is in the subspace sigma-algebra
-       induced by its domain.  (Contributed by Glauco Siliprandi,
-       26-Jun-2021.) $)
+       induced by its domain.  (Contributed by Glauco Siliprandi, 26-Jun-2021.)
+       (Revised by Glauco Siliprandi, 20-Dec-2024.) $)
     smfpimltxrmpt $p |- ( ph -> { x e. A | B < R } e. ( S |`t A ) ) $=
-      ( vy clt wbr crab crest wcel wceq nfcv co cv cmpt cfv cdm nfmpt1 nfdm nfv
-      nffv nfbr fveq2 breq1d cbvrabw a1i eqid smfpimltxr eqeltrd dmmptdf rabeqf
-      syl wa fvmpt2d rabbida eqidd 3eqtrrd eqcomd oveq2d eleq12d mpbird ) ADENO
-      ZBCPZFCQUAZRBUBZBCDUCZUDZENOZBVNUEZPZFVQQUAZRAVRMUBZVNUDZENOZMVQPZVSVRWCS
-      AVPWBBMVQBVNBCDUFZUGZMVQTVPMUHBWAENBVTVNWDBVTTUIBNTBETUJVMVTSVOWAENVMVTVN
-      UKULUMUNAMEVQFVNMVNTIKVQUOLUPUQAVKVRVLVSAVRVPBCPZVKVKAVQCSVRWFSABVNCDGHVN
-      UOZJURZVPBVQCWEBCTUSUTAVPVJBCHAVMCRVAVODENABCDVNGVNVNSAWGUNJVBULVCAVKVDVE
-      ACVQFQAVQCWHVFVGVHVI $.
+      ( nfcv smfpimltxrmptf ) ABCDEFGHBCMIJKLN $.
   $}
 
   ${
@@ -752220,6 +752342,29 @@ convergence can be decidedly irregular (Remark 121G of [Fremlin1]
       EEUOUAUBBUCTULDLMUKDLUNABUDCUKDUQTULDUKUEUFUGUKULUHUI $.
   $}
 
+  ${
+    $d A y $.  $d B y $.  $d L x y $.
+    smfpimgtxrmptf.x $e |- F/ x ph $.
+    smfpimgtxrmptf.1 $e |- F/_ x A $.
+    smfpimgtxrmptf.s $e |- ( ph -> S e. SAlg ) $.
+    smfpimgtxrmptf.b $e |- ( ( ph /\ x e. A ) -> B e. V ) $.
+    smfpimgtxrmptf.f $e |- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) ) $.
+    smfpimgtxrmptf.l $e |- ( ph -> L e. RR* ) $.
+    $( Given a function measurable w.r.t. to a sigma-algebra, the preimage of
+       an open interval unbounded above is in the subspace sigma-algebra
+       induced by its domain.  (Contributed by Glauco Siliprandi,
+       20-Dec-2024.) $)
+    smfpimgtxrmptf $p |- ( ph -> { x e. A | L < B } e. ( S |`t A ) ) $=
+      ( vy clt wbr crab wcel wceq nfcv crest co cv cmpt cfv cdm nfmpt1 nfdm nfv
+      nffv nfbr fveq2 breq2d cbvrabw a1i smfpimgtxr eqeltrd dmmptdf2 rabeqf syl
+      eqid wa simpr fvmpt2f syl2anc rabbida eqidd 3eqtrrd eqcomd oveq2d eleq12d
+      mpbird ) AFDOPZBCQZECUAUBZRFBUCZBCDUDZUEZOPZBVQUFZQZEVTUAUBZRAWAFNUCZVQUE
+      ZOPZNVTQZWBWAWFSAVSWEBNVTBVQBCDUGZUHZNVTTVSNUIBFWDOBFTBOTBWCVQWGBWCTUJUKV
+      PWCSVRWDFOVPWCVQULUMUNUOANFVTEVQNVQTJLVTVAMUPUQAVNWAVOWBAWAVSBCQZVNVNAVTC
+      SWAWISABVQCDGHIVQVAKURZVSBVTCWHIUSUTAVSVMBCHAVPCRZVBZVRDFOWLWKDGRVRDSAWKV
+      CKBCDGIVDVEUMVFAVNVGVHACVTEUAAVTCWJVIVJVKVL $.
+  $}
+
   ${
     $d A x y $.  $d B y $.  $d L x y $.
     smfpimgtxrmpt.x $e |- F/ x ph $.
@@ -752229,17 +752374,10 @@ convergence can be decidedly irregular (Remark 121G of [Fremlin1]
     smfpimgtxrmpt.l $e |- ( ph -> L e. RR* ) $.
     $( Given a function measurable w.r.t. to a sigma-algebra, the preimage of
        an open interval unbounded above is in the subspace sigma-algebra
-       induced by its domain.  (Contributed by Glauco Siliprandi,
-       26-Jun-2021.) $)
+       induced by its domain.  (Contributed by Glauco Siliprandi, 26-Jun-2021.)
+       (Revised by Glauco Siliprandi, 20-Dec-2024.) $)
     smfpimgtxrmpt $p |- ( ph -> { x e. A | L < B } e. ( S |`t A ) ) $=
-      ( vy clt wbr crab crest wcel wceq nfcv co cv cmpt cfv cdm nfmpt1 nfdm nfv
-      nffv nfbr fveq2 breq2d cbvrabw a1i eqid smfpimgtxr eqeltrd dmmptdf rabeqf
-      syl wa fvmpt2d rabbida eqidd 3eqtrrd eqcomd oveq2d eleq12d mpbird ) AFDNO
-      ZBCPZECQUAZRFBUBZBCDUCZUDZNOZBVNUEZPZEVQQUAZRAVRFMUBZVNUDZNOZMVQPZVSVRWCS
-      AVPWBBMVQBVNBCDUFZUGZMVQTVPMUHBFWANBFTBNTBVTVNWDBVTTUIUJVMVTSVOWAFNVMVTVN
-      UKULUMUNAMFVQEVNMVNTIKVQUOLUPUQAVKVRVLVSAVRVPBCPZVKVKAVQCSVRWFSABVNCDGHVN
-      UOZJURZVPBVQCWEBCTUSUTAVPVJBCHAVMCRVAVODFNABCDVNGVNVNSAWGUNJVBULVCAVKVDVE
-      ACVQEQAVQCWHVFVGVHVI $.
+      ( nfcv smfpimgtxrmptf ) ABCDEFGHBCMIJKLN $.
   $}
 
   ${