avoid ax-10 ax-12: cbvralsvw sbccomlem (#4986)

Author: icecream17

discouraged

@@ -15518,6 +15518,7 @@ New usage of "cbvraldvaOLD" is discouraged (0 uses).
 New usage of "cbvralf" is discouraged (2 uses).
 New usage of "cbvralsv" is discouraged (0 uses).
 New usage of "cbvralsvwOLD" is discouraged (0 uses).
+New usage of "cbvralsvwOLDOLD" is discouraged (0 uses).
 New usage of "cbvralv" is discouraged (2 uses).
 New usage of "cbvralv2" is discouraged (1 uses).
 New usage of "cbvreu" is discouraged (2 uses).
@@ -19218,6 +19219,7 @@ New usage of "sbcbi" is discouraged (2 uses).
 New usage of "sbcbiVD" is discouraged (0 uses).
 New usage of "sbcco" is discouraged (1 uses).
 New usage of "sbcco3g" is discouraged (0 uses).
+New usage of "sbccomlemOLD" is discouraged (0 uses).
 New usage of "sbceqalOLD" is discouraged (0 uses).
 New usage of "sbcgOLD" is discouraged (0 uses).
 New usage of "sbciedOLD" is discouraged (0 uses).
@@ -20342,7 +20344,8 @@ Proof modification of "cbvopab1vOLD" is discouraged (13 steps).
 Proof modification of "cbvopabvOLD" is discouraged (20 steps).
 Proof modification of "cbvrabwOLD" is discouraged (139 steps).
 Proof modification of "cbvraldvaOLD" is discouraged (16 steps).
-Proof modification of "cbvralsvwOLD" is discouraged (53 steps).
+Proof modification of "cbvralsvwOLD" is discouraged (20 steps).
+Proof modification of "cbvralsvwOLDOLD" is discouraged (53 steps).
 Proof modification of "cbvreuvwOLD" is discouraged (13 steps).
 Proof modification of "cbvreuwOLD" is discouraged (145 steps).
 Proof modification of "cbvrexdva2OLD" is discouraged (109 steps).
@@ -21614,6 +21617,7 @@ Proof modification of "sbc6gOLD" is discouraged (30 steps).
 Proof modification of "sbc8g" is discouraged (55 steps).
 Proof modification of "sbcbi" is discouraged (33 steps).
 Proof modification of "sbcbiVD" is discouraged (59 steps).
+Proof modification of "sbccomlemOLD" is discouraged (124 steps).
 Proof modification of "sbceqalOLD" is discouraged (73 steps).
 Proof modification of "sbcgOLD" is discouraged (8 steps).
 Proof modification of "sbciedOLD" is discouraged (16 steps).

set.mm

@@ -30816,10 +30816,14 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
     $( Change bound variable by using a substitution.  Version of ~ cbvralsv
        with a disjoint variable condition, which does not require ~ ax-13 .
        (Contributed by NM, 20-Nov-2005.)  Avoid ~ ax-13 .  (Revised by GG,
-       10-Jan-2024.)  (Proof shortened by Wolf Lammen, 8-Mar-2025.) $)
+       10-Jan-2024.)  (Proof shortened by Wolf Lammen, 8-Mar-2025.)  Avoid
+       ~ ax-10 , ~ ax-12 .  (Revised by SN, 21-Aug-2025.) $)
     cbvralsvw $p |- ( A. x e. A ph <-> A. y e. A [ y / x ] ph ) $=
-      ( wsb nfv nfs1v sbequ12 cbvralw ) AABCEBCDACFABCGABCHI $.
-    $( $j usage 'cbvralsvw' avoids 'ax-13'; $)
+      ( cv wcel wi wal wsb wral sb8v df-ral weq eleq1w imbi1d pm5.74i albii sb6
+      3bitr4i sbrimvw bitr2i bitri ) BEDFZAGZBHUDBCIZCHZABDJABCIZCDJZUDBCKABDLU
+      HCEDFZUGGZCHUFUGCDLUJUECUEUIAGZBCIZUJBCMZUDGZBHUMUKGZBHUEULUNUOBUMUDUKUMU
+      CUIABCDNOPQUDBCRUKBCRSUIABCTUAQUBS $.
+    $( $j usage 'cbvralsvw' avoids 'ax-10' 'ax-12' 'ax-13'; $)
 
     $( Change bound variable by using a substitution.  Version of ~ cbvrexsv
        with a disjoint variable condition, which does not require ~ ax-13 .
@@ -30828,14 +30832,21 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
     cbvrexsvw $p |- ( E. x e. A ph <-> E. y e. A [ y / x ] ph ) $=
       ( wsb nfv nfs1v sbequ12 cbvrexw ) AABCEBCDACFABCGABCHI $.
     $( $j usage 'cbvrexsvw' avoids 'ax-13'; $)
+
+    $( Obsolete version of ~ cbvralsvw as of 21-Aug-2025.  (Contributed by NM,
+       20-Nov-2005.)  Avoid ~ ax-13 .  (Revised by GG, 10-Jan-2024.)  (Proof
+       shortened by Wolf Lammen, 8-Mar-2025.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    cbvralsvwOLD $p |- ( A. x e. A ph <-> A. y e. A [ y / x ] ph ) $=
+      ( wsb nfv nfs1v sbequ12 cbvralw ) AABCEBCDACFABCGABCHI $.
   $}
 
   ${
     $d z x A $.  $d y A $.  $d z y ph $.  $d x y $.
     $( Obsolete version of ~ cbvralsvw as of 8-Mar-2025.  (Contributed by NM,
        20-Nov-2005.)  Avoid ~ ax-13 .  (Revised by GG, 10-Jan-2024.)
        (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    cbvralsvwOLD $p |- ( A. x e. A ph <-> A. y e. A [ y / x ] ph ) $=
+    cbvralsvwOLDOLD $p |- ( A. x e. A ph <-> A. y e. A [ y / x ] ph ) $=
       ( vz wral wsb nfv nfs1v sbequ12 cbvralw sbequ bitri ) ABDFABEGZEDFABCGZCD
       FANBEDAEHABEIABEJKNOECDNCHOEHAECBLKM $.
 
@@ -37186,9 +37197,27 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
   ${
     $d x y A $.  $d x y B $.
     $( Lemma for ~ sbccom .  (Contributed by NM, 14-Nov-2005.)  (Revised by
-       Mario Carneiro, 18-Oct-2016.) $)
+       Mario Carneiro, 18-Oct-2016.)  Avoid ~ ax-10 , ~ ax-12 .  (Revised by
+       SN, 20-Aug-2025.) $)
     sbccomlem $p |- ( [. A / x ]. [. B / y ]. ph
          <-> [. B / y ]. [. A / x ]. ph ) $=
+      ( cvv wcel wsbc wb sbcex cv wceq wi wal sbc6g isset exim biimtrid exlimiv
+      wex syl6com sylbid mpcom pm5.21ni bi2.04 2albii alcom bitri albii 3bitr3i
+      wa 19.21v a1i imbi2d albidv adantl adantr 3bitr4d ecase ) DFGZEFGZACEHZBD
+      HZABDHZCEHZIVCUTVEVBBDJZVAVEUTVDCEJZVAVECKELZVDMZCNZUTVDCEFOZVJVAVDCTZUTV
+      AVHCTVJVLCEPVHVDCQRVDUTCABDJSUAUBUCUDVCVAVEUTVCVAVFUTVCBKDLZVBMZBNZVAVBBD
+      FOZVOUTVBBTZVAUTVMBTVOVQBDPVMVBBQRVBVABACEJSUAUBUCVGUDUTVAUKZVOVJVCVEVRVM
+      VHAMZCNZMZBNZVHVMAMZBNZMZCNZVOVJWBWFIVRVMVSMZCNZBNZVHWCMZBNZCNZWBWFWIWJCN
+      BNWLWGWJBCVMVHAUEUFWJBCUGUHWHWABVMVSCULUIWKWECVHWCBULUIUJUMVAVOWBIUTVAVNW
+      ABVAVBVTVMACEFOUNUOUPUTVJWFIVAUTVIWECUTVDWDVHABDFOUNUOUQURUTVCVOIVAVPUQVA
+      VEVJIUTVKUPURUS $.
+    $( $j usage 'sbccomlem' avoids 'ax-10' 'ax-12'; $)
+
+    $( Obsolete version of ~ sbccomlem as of 20-Aug-2025.  (Contributed by NM,
+       14-Nov-2005.)  (Revised by Mario Carneiro, 18-Oct-2016.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    sbccomlemOLD $p |- ( [. A / x ]. [. B / y ]. ph
+         <-> [. B / y ]. [. A / x ]. ph ) $=
       ( cv wceq wa wex wsbc excom exdistr an12 exbii bitri 3bitr3i sbc5 3bitr4i
       19.42v sbcbii ) CFEGZAHZCIZBDJZBFDGZAHZBIZCEJZACEJZBDJABDJZCEJUEUCHBIZUAU
       GHZCIZUDUHUEUBHZCIBIUNBIZCIUKUMUNBCKUEUBBCLUOULCUOUAUFHZBIULUNUPBUEUAAMNU