shorten abid2f (#4677)

discouraged

@@ -14407,6 +14407,7 @@ New usage of "ab0ALT" is discouraged (0 uses).
 New usage of "ab0OLD" is discouraged (0 uses).
 New usage of "ab0orvALT" is discouraged (0 uses).
 New usage of "abfOLD" is discouraged (0 uses).
+New usage of "abid2fOLD" is discouraged (0 uses).
 New usage of "ablo32" is discouraged (4 uses).
 New usage of "ablo4" is discouraged (3 uses).
 New usage of "ablocom" is discouraged (6 uses).
@@ -19712,6 +19713,7 @@ Proof modification of "ab0ALT" is discouraged (33 steps).
 Proof modification of "ab0OLD" is discouraged (146 steps).
 Proof modification of "ab0orvALT" is discouraged (19 steps).
 Proof modification of "abfOLD" is discouraged (13 steps).
+Proof modification of "abid2fOLD" is discouraged (26 steps).
 Proof modification of "abn0OLD" is discouraged (28 steps).
 Proof modification of "abrexexgOLD" is discouraged (43 steps).
 Proof modification of "abscncfALT" is discouraged (71 steps).

set.mm

@@ -27320,16 +27320,6 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
     $( $j usage 'cleqf' avoids 'ax-10' 'ax-13'; $)
   $}
 
-  ${
-    abid2f.1 $e |- F/_ x A $.
-    $( A simplification of class abstraction.  Theorem 5.2 of [Quine] p. 35.
-       (Contributed by NM, 5-Sep-2011.)  (Revised by Mario Carneiro,
-       7-Oct-2016.)  (Proof shortened by Wolf Lammen, 17-Nov-2019.) $)
-    abid2f $p |- { x | x e. A } = A $=
-      ( cv wcel cab wceq wb nfab1 cleqf abid mpgbir ) ADZBEZAFZBGMOENHAAOBNAICJ
-      NAKL $.
-  $}
-
   ${
     eqabf.0 $e |- F/_ x A $.
     $( Equality of a class variable and a class abstraction.  In this version,
@@ -27342,6 +27332,24 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
     $( $j usage 'eqabf' avoids 'ax-13'; $)
   $}
 
+  ${
+    abid2f.1 $e |- F/_ x A $.
+    $( A simplification of class abstraction.  Theorem 5.2 of [Quine] p. 35.
+       (Contributed by NM, 5-Sep-2011.)  (Revised by Mario Carneiro,
+       7-Oct-2016.)  (Proof shortened by Wolf Lammen, 26-Feb-2025.) $)
+    abid2f $p |- { x | x e. A } = A $=
+      ( cv wcel cab wceq wb eqabf biid mpgbir eqcomi ) BADBEZAFZBNGMMHAMABCIMJK
+      L $.
+
+    $( Obsolete version of ~ abid2f as of 26-Feb-2025.  (Contributed by NM,
+       5-Sep-2011.)  (Revised by Mario Carneiro, 7-Oct-2016.)  (Proof shortened
+       by Wolf Lammen, 17-Nov-2019.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    abid2fOLD $p |- { x | x e. A } = A $=
+      ( cv wcel cab wceq wb nfab1 cleqf abid mpgbir ) ADZBEZAFZBGMOENHAAOBNAICJ
+      NAKL $.
+  $}
+
   ${
     $d v A $.  $d x z v $.  $d y z v $.  $d v ph $.
     sbabel.1 $e |- F/_ x A $.