Revise snnen2oOLD

discouraged

@@ -19099,6 +19099,7 @@ New usage of "sn-wcdeq" is discouraged (0 uses).
 New usage of "snatpsubN" is discouraged (3 uses).
 New usage of "snelpwrVD" is discouraged (0 uses).
 New usage of "snexALT" is discouraged (1 uses).
+New usage of "snnen2oOLD" is discouraged (0 uses).
 New usage of "snssiALT" is discouraged (0 uses).
 New usage of "snssiALTVD" is discouraged (0 uses).
 New usage of "snssl" is discouraged (0 uses).
@@ -21214,6 +21215,7 @@ Proof modification of "sn-00id" is discouraged (50 steps).
 Proof modification of "snelpwrVD" is discouraged (37 steps).
 Proof modification of "snex" is discouraged (64 steps).
 Proof modification of "snexALT" is discouraged (48 steps).
+Proof modification of "snnen2oOLD" is discouraged (116 steps).
 Proof modification of "snssiALT" is discouraged (40 steps).
 Proof modification of "snssiALTVD" is discouraged (64 steps).
 Proof modification of "snssl" is discouraged (18 steps).

set.mm

@@ -92579,16 +92579,6 @@ proved without using the Axiom of Power Sets (unlike ~ domsdomtr ).
     $( $j usage 'phpeqd' avoids 'ax-pow'; $)
   $}
 
-  $( A singleton ` { A } ` is never equinumerous with the ordinal number 2.
-     This holds for proper singletons ( ` A e. _V ` ) as well as for singletons
-     being the empty set ( ` A e/ _V ` ).  (Contributed by AV, 6-Aug-2019.) $)
-  snnen2o $p |- -. { A } ~~ 2o $=
-    ( cvv wcel csn c2o cen wbr wn c1o csuc com 1onn php5 ax-mp ensn1g wi ensymb
-    df-2o c0 wceq eqcomi breq2i entr ex sylbi con3rr3 sylnbi mpsyl 2on0 nemtbir
-    en0 bitri snprc biimpi breq1d mtbiri pm2.61i ) ABCZADZEFGZHZIIJZFGZHZURUSIF
-    GZVAIKCVDLIMNABOVCIEFGZVEVAPVBEIFEVBRUAUBVEUTVFVEIUSFGZUTVFPUSIQVGUTVFIUSEU
-    CUDUEUFUGUHURHZUTSEFGZVIESUIVIESFGESTSEQEUKULUJVHUSSEFVHUSSTAUMUNUOUPUQ $.
-
   $( Cardinal ordering agrees with ordinal number ordering when the smaller
      number is a natural number.  Compare with ~ nndomo when both are natural
      numbers.  (Contributed by NM, 17-Jun-1998.)  Generalize from ~ nndomo .
@@ -92774,6 +92764,16 @@ being the empty set ( ` A e/ _V ` ).  (Contributed by AV, 6-Aug-2019.) $)
     UTABNOABPSQUMARZBRZUQUSTUNAUJBUKVAVBFZUQBADZKUSABUAVCVDURVBVAVDURTBAUBUCUDU
     LUEUFUNUQUPLUMABEUGUHUI $.
 
+  $( Obsolete version of ~ snnen2o as of 18-Nov-2024.  (Contributed by AV,
+     6-Aug-2019.)  (Proof modification is discouraged.)
+     (New usage is discouraged.) $)
+  snnen2oOLD $p |- -. { A } ~~ 2o $=
+    ( cvv wcel csn c2o cen wbr wn c1o csuc com 1onn php5 ax-mp ensn1g wi ensymb
+    df-2o c0 wceq eqcomi breq2i entr ex sylbi con3rr3 sylnbi mpsyl 2on0 nemtbir
+    en0 bitri snprc biimpi breq1d mtbiri pm2.61i ) ABCZADZEFGZHZIIJZFGZHZURUSIF
+    GZVAIKCVDLIMNABOVCIEFGZVEVAPVBEIFEVBRUAUBVEUTVFVEIUSFGZUTVFPUSIQVGUTVFIUSEU
+    CUDUEUFUGUHURHZUTSEFGZVIESUIVIESFGESTSEQEUKULUJVHUSSEFVHUSSTAUMUNUOUPUQ $.
+
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -92897,6 +92897,23 @@ Finite sets (cont.)
       EWFXMXTFXSXPXRWGXHWSXLXSWHWIWNXHWSFERWJWKWLWMWOWPWQWR $.
   $}
 
+  ${
+    $d A f $.
+    $( A singleton ` { A } ` is never equinumerous with the ordinal number 2.
+       This holds for proper singletons ( ` A e. _V ` ) as well as for
+       singletons being the empty set ( ` A e/ _V ` ).  (Contributed by AV,
+       6-Aug-2019.)  Avoid ~ ax-pow , ~ ax-un .  (Revised by BTernaryTau,
+       1-Dec-2024.) $)
+    snnen2o $p |- -. { A } ~~ 2o $=
+      ( vf vx csn c2o cen wbr cv wf1o wex ccnv wf1 wceq c0 c1o cvv wcel wne nex
+      mto cpr df2o3 0ex 1oex 1n0 necomi prnesn mp3an eqnetri neii f1cdmsn mpan2
+      2on0 f1ocnv f1of1 syl wb snex 2oex breng mp2an mtbir ) ADZEFGZVCEBHZIZBJZ
+      VFBVFEVCVEKZLZVIECHZDZMZCJZVLCEVKENOUAZVKUBNPQOPQNORVNVKRUCUDONUEUFNOVJPP
+      UGUHUIUJSVIENRVMUMCEAVHUKULTVFEVCVHIVIVCEVEUNEVCVHUOUPTSVCPQEPQVDVGUQAURU
+      SVCEBPPUTVAVB $.
+    $( $j usage 'snnen2o' avoids 'ax-pow' 'ax-un'; $)
+  $}
+
   ${
     $d F w z $.  $d a b m n s t w x z $.
     unxpdomlem1.1 $e |- F = ( x e. ( a u. b ) |-> G ) $.