diff --git a/discouraged b/discouraged
index 36beba9f3..e32fb9e3b 100755
--- a/discouraged
+++ b/discouraged
@@ -9299,7 +9299,6 @@
 "mndomgmid" is used by "isdrngo2".
 "mndomgmid" is used by "ismndo2".
 "mndomgmid" is used by "rngoidmlem".
-"mo3OLD" is used by "mo4fOLD".
 "mpv" is used by "mulcompr".
 "mulassnq" is used by "1idpr".
 "mulassnq" is used by "addclprlem2".
@@ -16327,9 +16326,8 @@ New usage of "mndoisexid" is discouraged (2 uses).
 New usage of "mndoismgmOLD" is discouraged (3 uses).
 New usage of "mndoissmgrpOLD" is discouraged (1 uses).
 New usage of "mndomgmid" is discouraged (3 uses).
-New usage of "mo3OLD" is discouraged (1 uses).
+New usage of "mo3OLD" is discouraged (0 uses).
 New usage of "mo4OLD" is discouraged (0 uses).
-New usage of "mo4fOLD" is discouraged (0 uses).
 New usage of "moanimvOLD" is discouraged (0 uses).
 New usage of "mobiOLD" is discouraged (0 uses).
 New usage of "mobidOLD" is discouraged (0 uses).
@@ -18943,7 +18941,6 @@ Proof modification of "mndoismgmOLD" is discouraged (14 steps).
 Proof modification of "mndoissmgrpOLD" is discouraged (22 steps).
 Proof modification of "mo3OLD" is discouraged (163 steps).
 Proof modification of "mo4OLD" is discouraged (9 steps).
-Proof modification of "mo4fOLD" is discouraged (54 steps).
 Proof modification of "moanimvOLD" is discouraged (7 steps).
 Proof modification of "mobiOLD" is discouraged (63 steps).
 Proof modification of "mobidOLD" is discouraged (49 steps).
diff --git a/set.mm b/set.mm
index 78f6b857f..2e4f32a9c 100644
--- a/set.mm
+++ b/set.mm
@@ -1,5 +1,4 @@
 $( This is the Metamath database set.mm. $)
-
 $( Metamath is a formal language and associated computer program for
    archiving, verifying, and studying mathematical proofs, created by Norman
    Dwight Megill (1950--2021).  For more information, visit
@@ -17425,6 +17424,14 @@ disjoint variable condition ( ~ sb2 ).  Theorem ~ sb6f replaces the
       BDFZAGZBHZGDHBCFZAGZBHZABDCIRUADCOQTBOPSADCBJKLMN $.
   $}
 
+  ${
+    $d x y $.
+    $( One direction of ~ sb5 , provable from fewer axioms.  See also ~ sb1 .
+       (Contributed by Wolf Lammen, 20-Jan-2024.) $)
+    sb1v $p |- ( [ y / x ] ph -> E. x ( x = y /\ ph ) ) $=
+      ( wsb weq wi wal wa wex sb6 equs4v sylbi ) ABCDBCEZAFBGMAHBIABCJABCKL $.
+  $}
+
   ${
     $d x y $.
     $( Obsolete as of 30-Jul-2023.  Use ~ sb6 instead.  (Contributed by BJ,
@@ -19265,10 +19272,10 @@ Converse of the inference rule of (universal) generalization ~ ax-gen .
     $d x y $.
     $( Alternate definition of substitution when variables are disjoint.
        Similar to Theorem 6.1 of [Quine] p. 40.  The implication "to the right"
-       is ~ sb1 and does not require any disjoint variable condition.  Theorem
-       ~ sb5f replaces the disjoint variable condition with a non-freeness
-       hypothesis.  (Contributed by NM, 18-Aug-1993.)  Shorten ~ sb56 .
-       (Revised by Wolf Lammen, 4-Sep-2023.) $)
+       is ~ sb1v and even needs no disjoint variable condition, see ~ sb1 .
+       Theorem ~ sb5f replaces the disjoint variable condition with a
+       non-freeness hypothesis.  (Contributed by NM, 18-Aug-1993.)  Shorten
+       ~ sb56 .  (Revised by Wolf Lammen, 4-Sep-2023.) $)
     sb5 $p |- ( [ y / x ] ph <-> E. x ( x = y /\ ph ) ) $=
       ( weq wa wex wsb nfs1v sbequ12 equsexv bicomi ) BCDAEBFABCGZALBCABCHABCIJ
       K $.
@@ -22992,13 +22999,6 @@ derived from that of uniqueness ( ~ df-mo ).  (Contributed by Wolf
     mo4f $p |- ( E* x ph <-> A. x A. y ( ( ph /\ ps ) -> x = y ) ) $=
       ( wmo wsb wa weq wi wal nfv mo3 sbiev anbi2i imbi1i 2albii bitri ) ACGAAC
       DHZIZCDJZKZDLCLABIZUBKZDLCLACDADMNUCUECDUAUDUBTBAABCDEFOPQRS $.
-
-    $( Obsolete version of ~ mo4f as of 19-Jan-2023.  (Contributed by NM,
-       10-Apr-2004.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    mo4fOLD $p |- ( E* x ph <-> A. x A. y ( ( ph /\ ps ) -> x = y ) ) $=
-      ( wmo wsb wa weq wi wal nfv mo3OLD sbie anbi2i imbi1i 2albii bitri ) ACGA
-      ACDHZIZCDJZKZDLCLABIZUBKZDLCLACDADMNUCUECDUAUDUBTBAABCDEFOPQRS $.
   $}
 
   ${
@@ -229301,7 +229301,7 @@ U C_ ( T .(+) U ) ) $=
       ( csubg cfv wcel csubmnd co wceq subgsubm smndlsmidm syl ) BCEFGBCHFGBBAI
       BJBCKABCDLM $.
 
-    $( Obsolete proof of ~ lsmidm as of 13-Jan-2023.  Subgroup sum is
+    $( Obsolete proof of ~ lsmidm as of 13-Jan-2024.  Subgroup sum is
        idempotent.  (Contributed by NM, 6-Feb-2014.)  (Revised by Mario
        Carneiro, 21-Jun-2014.)  (New usage is discouraged.)
        (Proof modification is discouraged.) $)