revise clelsb2 (#4433)

* revise clelsb2

* add usage tag

* typo

discouraged

@@ -12837,7 +12837,7 @@
 "sbco" is used by "sbid2".
 "sbco2" is used by "cbvab".
 "sbco2" is used by "clelsb1f".
-"sbco2" is used by "clelsb2".
+"sbco2" is used by "clelsb2OLD".
 "sbco2" is used by "sb7f".
 "sbco2" is used by "sbcco".
 "sbco2" is used by "sbco2d".
@@ -12866,7 +12866,7 @@
 "sbie" is used by "cbvreu".
 "sbie" is used by "cbvreucsf".
 "sbie" is used by "cbvriota".
-"sbie" is used by "clelsb2".
+"sbie" is used by "clelsb2OLD".
 "sbie" is used by "nd1".
 "sbie" is used by "nd2".
 "sbie" is used by "nfcdeq".
@@ -15673,6 +15673,7 @@ New usage of "clelabOLD" is discouraged (0 uses).
 New usage of "cleljustALT" is discouraged (0 uses).
 New usage of "cleljustALT2" is discouraged (0 uses).
 New usage of "clelsb1f" is discouraged (0 uses).
+New usage of "clelsb2OLD" is discouraged (0 uses).
 New usage of "clmgmOLD" is discouraged (1 uses).
 New usage of "cm0" is discouraged (1 uses).
 New usage of "cm2j" is discouraged (1 uses).
@@ -20015,6 +20016,7 @@ Proof modification of "clel4OLD" is discouraged (24 steps).
 Proof modification of "clelabOLD" is discouraged (75 steps).
 Proof modification of "cleljustALT" is discouraged (25 steps).
 Proof modification of "cleljustALT2" is discouraged (25 steps).
+Proof modification of "clelsb2OLD" is discouraged (63 steps).
 Proof modification of "clmgmOLD" is discouraged (50 steps).
 Proof modification of "cnaddabloOLD" is discouraged (65 steps).
 Proof modification of "cnaddcom" is discouraged (71 steps).

set.mm

@@ -26528,11 +26528,19 @@ atomic formula (class version of ~ elsb1 ).  (Contributed by Rodolfo
   $}
 
   ${
-    $d w x A $.  $d w y $.
+    $d w x z A $.  $d w y z $.
     $( Substitution for the second argument of the membership predicate in an
        atomic formula (class version of ~ elsb2 ).  (Contributed by Jim
-       Kingdon, 22-Nov-2018.) $)
+       Kingdon, 22-Nov-2018.)  Reduce dependencies on axioms.  (Revised by Wolf
+       Lammen, 24-Nov-2024.) $)
     clelsb2 $p |- ( [ y / x ] A e. x <-> A e. y ) $=
+      ( vz cv wcel eleq2w sbievw2 ) CAEFCBEFCDEFABDADCGDBCGH $.
+    $( $j usage 'clelsb2' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13' 'ax-ext'; $)
+
+    $( Obsolete version of ~ clelsb2 as of 24-Nov-2024.)  (Contributed by Jim
+       Kingdon, 22-Nov-2018.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    clelsb2OLD $p |- ( [ y / x ] A e. x <-> A e. y ) $=
       ( vw cv wcel wsb nfv sbco2 eleq2 sbie sbbii 3bitr3i ) CDEZFZDAGZABGODBGCA
       EZFZABGCBEZFZODBAOAHIPRABORDARDHNQCJKLOTDBTDHNSCJKM $.
   $}