One direction of sb5 is provable from fewer axioms

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".
@@ -16110,7 +16109,6 @@ New usage of "lsatfixedN" is discouraged (1 uses).
 New usage of "lshpinN" is discouraged (0 uses).
 New usage of "lshpnel2N" is discouraged (0 uses).
 New usage of "lshpset2N" is discouraged (1 uses).
-New usage of "lsmidmOLD" is discouraged (0 uses).
 New usage of "ltaddnq" is discouraged (7 uses).
 New usage of "ltaddpr" is discouraged (5 uses).
 New usage of "ltaddpr2" is discouraged (1 uses).
@@ -16327,9 +16325,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).
@@ -18874,7 +18871,6 @@ Proof modification of "latmassOLD" is discouraged (309 steps).
 Proof modification of "lcmftp" is discouraged (1057 steps).
 Proof modification of "lediv2aALT" is discouraged (264 steps).
 Proof modification of "leibpilem1OLD" is discouraged (254 steps).
-Proof modification of "lsmidmOLD" is discouraged (116 steps).
 Proof modification of "luk-1" is discouraged (73 steps).
 Proof modification of "luk-2" is discouraged (52 steps).
 Proof modification of "luk-3" is discouraged (20 steps).
@@ -18943,7 +18939,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).

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
@@ -22992,13 +22991,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,17 +229293,6 @@ 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
-       idempotent.  (Contributed by NM, 6-Feb-2014.)  (Revised by Mario
-       Carneiro, 21-Jun-2014.)  (New usage is discouraged.)
-       (Proof modification is discouraged.) $)
-    lsmidmOLD $p |- ( U e. ( SubGrp ` G ) -> ( U .(+) U ) = U ) $=
-      ( vx vy csubg cfv wcel co cv cplusg cmpo crn wceq eqid lsmval anidms wral
-      cbs cxp subgcl 3expb ralrimivva fmpo sylib frnd eqsstrd wss lsmub1 eqssd
-      wf ) BCGHIZBBAJZBUMUNEFBBEKZFKZCLHZJZMZNZBUMUNUTOEFCTHZUQABBCVAPUQPZDQRUM
-      BBUAZBUSUMURBIZFBSEBSVCBUSULUMVDEFBBUMUOBIUPBIVDUQBCUOUPVBUBUCUDEFBBURBUS
-      USPUEUFUGUHUMBUNUIABBCDUJRUK $.
-
     $( The least upper bound property of subgroup sum.  (Contributed by NM,
        6-Feb-2014.)  (Revised by Mario Carneiro, 21-Jun-2014.) $)
     lsmlub $p |- ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\
@@ -541596,6 +541577,14 @@ dependency is expressed in our hypothesis (called implicit
       UGCBUGCLMABCNOUCUEABUECBHAICJZUCAACBPUCUHAACBNQRSTUA $.
   $}
 
+  ${
+    $d x y $.
+    $( One direction of ~ sb5 is provable from fewer axioms.  See also ~ sb1 .
+       (Contributed by Wolf Lammen, 20-Jan-2024.) $)
+    wl-sb1v $p |- ( [ y / x ] ph -> E. x ( x = y /\ ph ) ) $=
+      ( wsb weq wi wal wa wex sb6 equs4v sylbi ) ABCDBCEZAFBGMAHBIABCJABCKL $.
+  $}
+
   $( A specialization of ~ wl-equsal1t .  Closed form of ~ sb6rf .
      (Contributed by Wolf Lammen, 27-Jul-2019.) $)
   wl-sb6rft $p |- ( F/ x ph -> ( ph <-> A. x ( x = y -> [ x / y ] ph ) ) ) $=