prove nfceqi without ax-12 (#3262)

Co-authored-by: Wolf Lammen <[email protected]>

Author: wlammen

discouraged

@@ -16600,6 +16600,7 @@ New usage of "nfabd2OLD" is discouraged (0 uses).
 New usage of "nfabdOLD" is discouraged (0 uses).
 New usage of "nfan1OLDOLD" is discouraged (0 uses).
 New usage of "nfbii2OLD" is discouraged (0 uses).
+New usage of "nfceqiOLD" is discouraged (0 uses).
 New usage of "nfcvfOLD" is discouraged (0 uses).
 New usage of "nfeqf2OLD" is discouraged (0 uses).
 New usage of "nfeqf2OLDOLD" is discouraged (0 uses).
@@ -19393,6 +19394,7 @@ Proof modification of "nfabd2OLD" is discouraged (75 steps).
 Proof modification of "nfabdOLD" is discouraged (18 steps).
 Proof modification of "nfan1OLDOLD" is discouraged (33 steps).
 Proof modification of "nfbii2OLD" is discouraged (15 steps).
+Proof modification of "nfceqiOLD" is discouraged (21 steps).
 Proof modification of "nfcvfOLD" is discouraged (18 steps).
 Proof modification of "nfeqf2OLD" is discouraged (65 steps).
 Proof modification of "nfeqf2OLDOLD" is discouraged (52 steps).

set.mm

@@ -26069,10 +26069,25 @@ choice between (what we call) a "definitional form" where the shorter
   $}
 
   ${
+    $d x y $.  $d A y $.  $d B y $.
     nfceqi.1 $e |- A = B $.
     $( Equality theorem for class not-free.  (Contributed by Mario Carneiro,
-       11-Aug-2016.)  (Proof shortened by Wolf Lammen, 16-Nov-2019.) $)
+       11-Aug-2016.)  (Proof shortened by Wolf Lammen, 16-Nov-2019.)  Avoid
+       ~ ax-12 .  (Revised by Wolf Lammen, 19-Jun-2023.) $)
     nfceqi $p |- ( F/_ x A <-> F/_ x B ) $=
+      ( vy cv wcel wnf wal wnfc eleq2i nfbii albii df-nfc 3bitr4i ) EFZBGZAHZEI
+      PCGZAHZEIABJACJRTEQSABCPDKLMAEBNAECNO $.
+
+    $( $j usage 'nfceqi' avoids 'ax-8' 'ax-10' 'ax-11' 'ax-12' 'ax-13' ; $)
+  $}
+
+
+  ${
+    nfcxfr.1 $e |- A = B $.
+    $( Obsolete proof of ~ nfceqi as of 19-Jun-2023.  (Contributed by Mario
+       Carneiro, 11-Aug-2016.)  (Proof shortened by Wolf Lammen, 16-Nov-2019.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    nfceqiOLD $p |- ( F/_ x A <-> F/_ x B ) $=
       ( wnfc wb wtru nftru wceq a1i nfceqdf mptru ) ABEACEFGABCAHBCIGDJKL $.
 
     ${