remove ax-10:mopick; ax-10+ax-12:dfdif3 (#4977)

* prove+use ax12ev2

automatic usage in mopick saves ax-10

* shorten dfdif3 (rmv axioms)

Author: icecream17

discouraged

@@ -16201,6 +16201,7 @@ New usage of "dfbi1ALT" is discouraged (0 uses).
 New usage of "dfch2" is discouraged (0 uses).
 New usage of "dfcnfldOLD" is discouraged (13 uses).
 New usage of "dfcnqs" is discouraged (4 uses).
+New usage of "dfdif3OLD" is discouraged (0 uses).
 New usage of "dfeu" is discouraged (0 uses).
 New usage of "dffr2ALT" is discouraged (0 uses).
 New usage of "dffun2OLD" is discouraged (0 uses).
@@ -19202,6 +19203,7 @@ New usage of "sb9i" is discouraged (0 uses).
 New usage of "sbabelOLD" is discouraged (0 uses).
 New usage of "sbal1" is discouraged (0 uses).
 New usage of "sbal2" is discouraged (2 uses).
+New usage of "sbalexOLD" is discouraged (0 uses).
 New usage of "sbc2ieOLD" is discouraged (0 uses).
 New usage of "sbc2rexgOLD" is discouraged (1 uses).
 New usage of "sbc3or" is discouraged (1 uses).
@@ -20440,6 +20442,7 @@ Proof modification of "demoivreALT" is discouraged (1087 steps).
 Proof modification of "dfac5lem4OLD" is discouraged (689 steps).
 Proof modification of "dfbi1ALT" is discouraged (100 steps).
 Proof modification of "dfcnfldOLD" is discouraged (195 steps).
+Proof modification of "dfdif3OLD" is discouraged (137 steps).
 Proof modification of "dfeu" is discouraged (35 steps).
 Proof modification of "dffr2ALT" is discouraged (64 steps).
 Proof modification of "dffun2OLD" is discouraged (109 steps).
@@ -21594,6 +21597,7 @@ Proof modification of "sb5OLD" is discouraged (25 steps).
 Proof modification of "sb8fOLD" is discouraged (17 steps).
 Proof modification of "sbabelOLD" is discouraged (126 steps).
 Proof modification of "sbal1" is discouraged (149 steps).
+Proof modification of "sbalexOLD" is discouraged (32 steps).
 Proof modification of "sbc2ieOLD" is discouraged (38 steps).
 Proof modification of "sbc2or" is discouraged (134 steps).
 Proof modification of "sbc2rexgOLD" is discouraged (62 steps).

set.mm

@@ -18650,6 +18650,17 @@ This axiom scheme is logically redundant (see ~ ax12w ) but is used as an
     $( $j usage 'ax12v2' avoids 'ax-10' 'ax-11' 'ax-13'; $)
   $}
 
+  ${
+    $d x y $.
+    $( Version of ~ ax12v2 rewritten to use an existential quantifier.  One
+       direction of ~ sbalex without the universal quantifier, avoiding
+       ~ ax-10 .  (Contributed by SN, 14-Aug-2025.) $)
+    ax12ev2 $p |- ( E. x ( x = y /\ ph ) -> ( x = y -> ph ) ) $=
+      ( weq wa wex wn wi wal exnalimn ax12v2 con1d biimtrid com12 ) BCDZOAEBFZA
+      POAGZHBIZGOAOABJOARQBCKLMN $.
+    $( $j usage 'ax12ev2' avoids 'ax-10' 'ax-11' 'ax-13'; $)
+  $}
+
   ${
     $d x y $.  $d y ph $.
     $( If a wff is true, it is true for at least one instance.  Special case of
@@ -19231,11 +19242,20 @@ disjoint variable condition if we allow more axioms (see ~ equs4 ).
        nonfreeness hypothesis of ` t ` in ` ph ` .  (Contributed by NM,
        14-Apr-2008.)  Revised to use ~ equsexv in place of ~ equsex in order to
        remove dependency on ~ ax-13 .  (Revised by BJ, 20-Dec-2020.)  Revise to
-       remove dependency on ~ df-sb .  (Revised by BJ, 21-Sep-2024.) $)
+       remove dependency on ~ df-sb .  (Revised by BJ, 21-Sep-2024.)  (Proof
+       shortened by SN, 14-Aug-2025.) $)
     sbalex $p |- ( E. x ( x = t /\ ph ) <-> A. x ( x = t -> ph ) ) $=
+      ( weq wa wex wi wal nfe1 ax12ev2 alrimi equs4v impbii ) BCDZAEZBFZNAGZBHP
+      QBOBIABCJKABCLM $.
+    $( $j usage 'sbalex' avoids 'ax-11' 'df-sb' 'ax-13'; $)
+
+    $( Obsolete version of ~ sbalex as of 14-Aug-2025.  (Contributed by NM,
+       14-Apr-2008.)  (Revised by BJ, 20-Dec-2020.)  (Revised by BJ,
+       21-Sep-2024.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    sbalexOLD $p |- ( E. x ( x = t /\ ph ) <-> A. x ( x = t -> ph ) ) $=
       ( weq wa wex wi wal nfa1 ax12v2 imp exlimi equs4v impbii ) BCDZAEZBFOAGZB
       HZPRBQBIOARABCJKLABCMN $.
-    $( $j usage 'sbalex' avoids 'ax-11' 'df-sb' 'ax-13'; $)
   $}
 
   ${
@@ -23378,9 +23398,10 @@ of the unique existential quantifier (note that ` y ` and ` z ` need not
        quantifier.  (Contributed by NM, 27-Jan-1997.)  (Proof shortened by Wolf
        Lammen, 17-Sep-2019.) $)
     mopick $p |- ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( ph -> ps ) ) $=
-      ( vy wmo wa wex wi weq wal df-mo pm3.45 aleximi sbalex sylbi syl6 exlimiv
-      sp syl5d imp ) ACEZABFZCGZABHZUAACDIZHZCJZDGUCUDHZACDKUGUHDUGAUEUCBUFCRUG
-      UCUEBFZCGZUEBHZUFUBUICAUEBLMUJUKCJUKBCDNUKCROPSQOT $.
+      ( vy wmo wa wex wi weq df-mo sp pm3.45 aleximi ax12ev2 syl6 syl5d exlimiv
+      wal sylbi imp ) ACEZABFZCGZABHZUAACDIZHZCRZDGUCUDHZACDJUGUHDUGAUEUCBUFCKU
+      GUCUEBFZCGUEBHUFUBUICAUEBLMBCDNOPQST $.
+    $( $j usage 'mopick' avoids 'ax-10'; $)
   $}
 
   ${
@@ -39488,8 +39509,16 @@ many things are technically classes despite morally (and provably) being
   ${
     $d A x $.  $d B x y $.
     $( Alternate definition of class difference.  (Contributed by BJ and Jim
-       Kingdon, 16-Jun-2022.) $)
+       Kingdon, 16-Jun-2022.)  (Proof shortened by SN, 15-Aug-2025.) $)
     dfdif3 $p |- ( A \ B ) = { x e. A | A. y e. B x =/= y } $=
+      ( cv wcel wn wne wral cdif dfdif2 nelb necom ralbii bitri rabbieq ) AEZDF
+      GZQBEZHZBDIZACCDJACDKRSQHZBDIUABQDLUBTBDSQMNOP $.
+    $( $j usage 'dfdif3' avoids 'ax-10' 'ax-11' 'ax-12'; $)
+
+    $( Obsolete version of ~ dfdif3 as of 15-Aug-2025.  (Contributed by BJ and
+       Jim Kingdon, 16-Jun-2022.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    dfdif3OLD $p |- ( A \ B ) = { x e. A | A. y e. B x =/= y } $=
       ( cdif cv wcel wn crab wne wral dfdif2 wi wal weq wex ax6ev bitr4i 3bitri
       wa biantrur 19.41v sbalex equcom imbi1i eleq1w notbid pm5.74i con2b df-ne
       bicomi imbi2i bitri albii df-ral rabbii eqtri ) CDEAFZDGZHZACIURBFZJZBDKZ
@@ -694129,8 +694158,7 @@ D Fn ( I ... ( M - 1 ) ) /\
     $( Inference form of ~ sbalex , avoiding ~ ax-10 by using ~ ax-gen .
        (Contributed by SN, 12-Aug-2025.) $)
     sbalexi $p |- A. x ( x = y -> ph ) $=
-      ( weq wi wn wal wa wex exnalimn mpbi ax12v2 mt3i ax-gen ) BCEZAFBPAPAGZFB
-      HZPAIBJRGDPABKLQBCMNO $.
+      ( weq wi wa wex ax12ev2 ax-mp ax-gen ) BCEZAFZBLAGBHMDABCIJK $.
     $( $j usage 'sbalexi' avoids 'ax-10'; $)
   $}