janitorial stuff (#4241)

discouraged

@@ -17252,7 +17252,6 @@ New usage of "mndoissmgrpOLD" is discouraged (1 uses).
 New usage of "mndomgmid" is discouraged (3 uses).
 New usage of "mo4OLD" is discouraged (0 uses).
 New usage of "mobidvALT" is discouraged (0 uses).
-New usage of "mobiiOLD" is discouraged (0 uses).
 New usage of "moexex" is discouraged (2 uses).
 New usage of "moexexv" is discouraged (0 uses).
 New usage of "mof0ALT" is discouraged (0 uses).
@@ -19985,7 +19984,6 @@ Proof modification of "mndoismgmOLD" is discouraged (14 steps).
 Proof modification of "mndoissmgrpOLD" is discouraged (22 steps).
 Proof modification of "mo4OLD" is discouraged (9 steps).
 Proof modification of "mobidvALT" is discouraged (48 steps).
-Proof modification of "mobiiOLD" is discouraged (17 steps).
 Proof modification of "mof0ALT" is discouraged (67 steps).
 Proof modification of "mpjao3danOLD" is discouraged (29 steps).
 Proof modification of "mpofunOLD" is discouraged (95 steps).

set.mm

@@ -22548,12 +22548,6 @@ derived from that of uniqueness ( ~ df-mo ).  (Contributed by Wolf
     mobii $p |- ( E* x ps <-> E* x ch ) $=
       ( wmo biimpri moimi biimpi impbii ) ACEBCEBACABDFGABCABDHGI $.
     $( $j usage 'mobii' avoids 'ax-5'; $)
-
-    $( Obsolete version of ~ mobii as of 24-Sep-2023.  (Contributed by NM,
-       9-Mar-1995.)  (Revised by Mario Carneiro, 17-Oct-2016.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    mobiiOLD $p |- ( E* x ps <-> E* x ch ) $=
-      ( wb wmo mobi mpg ) ABEACFBCFECABCGDH $.
   $}
 
   ${
@@ -28448,7 +28442,7 @@ generally appear in a single form (either definitional, but more often
        Carneiro, 17-Oct-2016.)  (Proof shortened by Wolf Lammen,
        4-Dec-2019.) $)
     ralbii $p |- ( A. x e. A ph <-> A. x e. A ps ) $=
-      ( cv wcel imbi2i ralbii2 ) ABCDDABCFDGEHI $.
+      ( wb cv wcel a1i ralbiia ) ABCDABFCGDHEIJ $.
 
     $( Inference adding two restricted universal quantifiers to both sides of
        an equivalence.  (Contributed by NM, 1-Aug-2004.) $)
@@ -29201,9 +29195,8 @@ generally appear in a single form (either definitional, but more often
        8-Jun-2011.)  Reduce axiom dependencies.  (Revised by BJ,
        13-Jun-2019.) $)
     rexcom4 $p |- ( E. x e. A E. y ph <-> E. y E. x e. A ph ) $=
-      ( wex wrex cv wcel wa df-rex 19.42v bicomi exbii excom bitri ) ACEZBDFBGD
-      HZPIZBEZABDFZCEZPBDJSQAIZCEZBEZUARUCBUCRQACKLMUDUBBEZCEUAUBBCNUETCTUEABDJ
-      LMOOO $.
+      ( cv wcel wa wex wrex exdistr df-rex exbii excom bitri 3bitr4ri ) BEDFZAG
+      ZCHBHZPACHZGBHABDIZCHZSBDIPABCJUAQBHZCHRTUBCABDKLQCBMNSBDKO $.
   $}
 
   ${