prove abeq2f without ax-13 (#3173)

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

Author: wlammen

discouraged

@@ -13398,6 +13398,7 @@ New usage of "abbidOLD" is discouraged (0 uses).
 New usage of "abbidvOLD" is discouraged (0 uses).
 New usage of "abbiiOLD" is discouraged (0 uses).
 New usage of "abbiiOLDOLD" is discouraged (0 uses).
+New usage of "abeq2fOLD" 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).
@@ -16648,7 +16649,6 @@ New usage of "nfimdOLDOLD" is discouraged (0 uses).
 New usage of "nfmo1OLD" is discouraged (0 uses).
 New usage of "nfmod2OLD" is discouraged (0 uses).
 New usage of "nfnbiOLD" is discouraged (0 uses).
-New usage of "nfnfcALT" is discouraged (0 uses).
 New usage of "nfopdALT" is discouraged (0 uses).
 New usage of "nfs1vOLD" is discouraged (0 uses).
 New usage of "nfunidALT" is discouraged (0 uses).
@@ -18277,6 +18277,7 @@ Proof modification of "abbidOLD" is discouraged (24 steps).
 Proof modification of "abbidvOLD" is discouraged (9 steps).
 Proof modification of "abbiiOLD" is discouraged (38 steps).
 Proof modification of "abbiiOLDOLD" is discouraged (17 steps).
+Proof modification of "abeq2fOLD" is discouraged (46 steps).
 Proof modification of "abscncfALT" is discouraged (71 steps).
 Proof modification of "ackm" is discouraged (71 steps).
 Proof modification of "ad5ant123OLD" is discouraged (45 steps).
@@ -19464,7 +19465,6 @@ Proof modification of "nfimdOLDOLD" is discouraged (19 steps).
 Proof modification of "nfmo1OLD" is discouraged (25 steps).
 Proof modification of "nfmod2OLD" is discouraged (35 steps).
 Proof modification of "nfnbiOLD" is discouraged (46 steps).
-Proof modification of "nfnfcALT" is discouraged (30 steps).
 Proof modification of "nfopdALT" is discouraged (70 steps).
 Proof modification of "nfs1vOLD" is discouraged (10 steps).
 Proof modification of "nfunidALT" is discouraged (33 steps).

set.mm

@@ -26056,14 +26056,42 @@ choice between (what we call) a "definitional form" where the shorter
       ( wnfc cv wcel wnf wal df-nfc sp sylbi ) ACDBECFAGZBHLABCILBJK $.
   $}
 
+  ${
+    $d x y $.  $d y A $.
+    nfcriv.1 $e |- F/_ x A $.
+    $( Consequence of the not-free predicate, similiar to ~ nfcri .  Requires
+       ` y ` and ` A ` be disjoint, but is not based on ~ ax-13 .  (Contributed
+       by Wolf Lammen, 13-May-2023.) $)
+    nfcriv $p |- F/ x y e. A $=
+      ( wnfc cv wcel wnf nfcr ax-mp ) ACEBFCGAHDABCIJ $.
+  $}
+
+  ${
+    $d x y $.  $d y A $.
+    nfcd.1 $e |- F/ y ph $.
+    nfcd.2 $e |- ( ph -> F/ x y e. A ) $.
+    $( Deduce that a class ` A ` does not have ` x ` free in it.  (Contributed
+       by Mario Carneiro, 11-Aug-2016.) $)
+    nfcd $p |- ( ph -> F/_ x A ) $=
+      ( cv wcel wnf wal wnfc alrimi df-nfc sylibr ) ACGDHBIZCJBDKAOCEFLBCDMN $.
+  $}
+
+  ${
+    $d x y $.  $d y A $.
+    nfcrd.1 $e |- ( ph -> F/_ x A ) $.
+    $( Consequence of the not-free predicate.  (Contributed by Mario Carneiro,
+       11-Aug-2016.) $)
+    nfcrd $p |- ( ph -> F/ x y e. A ) $=
+      ( wnfc cv wcel wnf nfcr syl ) ABDFCGDHBIEBCDJK $.
+  $}
+
   ${
     $d x y z $.  $d z A $.
     nfcri.1 $e |- F/_ x A $.
     $( Consequence of the not-free predicate.  (Contributed by Mario Carneiro,
        11-Aug-2016.) $)
     nfcrii $p |- ( y e. A -> A. x y e. A ) $=
-      ( vz cv wcel wnfc wnf nfcr ax-mp nf5ri hblem ) AEBCEFCGZAACHNAIDAECJKLM
-      $.
+      ( vz cv wcel nfcriv nf5ri hblem ) AEBCEFCGAAECDHIJ $.
 
     $( Consequence of the not-free predicate.  (Note that unlike ~ nfcr , this
        does not require ` y ` and ` A ` to be disjoint.)  (Contributed by Mario
@@ -26072,16 +26100,6 @@ choice between (what we call) a "definitional form" where the shorter
       ( cv wcel nfcrii nf5i ) BECFAABCDGH $.
   $}
 
-  ${
-    $d x y $.  $d y A $.
-    nfcd.1 $e |- F/ y ph $.
-    nfcd.2 $e |- ( ph -> F/ x y e. A ) $.
-    $( Deduce that a class ` A ` does not have ` x ` free in it.  (Contributed
-       by Mario Carneiro, 11-Aug-2016.) $)
-    nfcd $p |- ( ph -> F/_ x A ) $=
-      ( cv wcel wnf wal wnfc alrimi df-nfc sylibr ) ACGDHBIZCJBDKAOCEFLBCDMN $.
-  $}
-
   ${
     $d x y $.  $d A y $.  $d B y $.  $d ph y $.
     nfceqdf.1 $e |- F/ x ph $.
@@ -26179,14 +26197,8 @@ choice between (what we call) a "definitional form" where the shorter
     ( wal nfa1 nfab ) ABDBCABEF $.
 
   ${
-    $d x y $.  $d y A $.  $d y B $.
+    $d x y $.  $d y A $.  $d y B $.  $d y ph $.
     nfeqd.1 $e |- ( ph -> F/_ x A ) $.
-    $( Consequence of the not-free predicate.  (Contributed by Mario Carneiro,
-       11-Aug-2016.) $)
-    nfcrd $p |- ( ph -> F/ x y e. A ) $=
-      ( wnfc cv wcel wnf nfcr syl ) ABDFCGDHBIEBCDJK $.
-
-    $d y ph $.
     nfeqd.2 $e |- ( ph -> F/_ x B ) $.
     $( Hypothesis builder for equality.  (Contributed by Mario Carneiro,
        7-Oct-2016.) $)
@@ -26208,15 +26220,8 @@ choice between (what we call) a "definitional form" where the shorter
        11-Aug-2016.)  Remove dependency on ~ ax-13 .  (Revised by Wolf Lammen,
        10-Dec-2019.) $)
     nfnfc $p |- F/ x F/_ y A $=
-      ( vz wnfc cv wcel wnf wal df-nfc nfcr ax-mp nfnf nfal nfxfr ) BCFEGCHZBIZ
-      EJABECKRAEQABACFQAIDAECLMNOP $.
-
-    $( Alternate proof of ~ nfnfc .  Shorter but requiring more axioms.
-       (Contributed by Mario Carneiro, 11-Aug-2016.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    nfnfcALT $p |- F/ x F/_ y A $=
-      ( vz wnfc cv wcel wnf wal df-nfc nfcri nfnf nfal nfxfr ) BCFEGCHZBIZEJABE
-      CKQAEPABAECDLMNO $.
+      ( vz wnfc cv wcel wnf wal df-nfc nfcriv nfnf nfal nfxfr ) BCFEGCHZBIZEJAB
+      ECKQAEPABAECDLMNO $.
 
     nfeq.2 $e |- F/_ x B $.
     $( Hypothesis builder for equality.  (Contributed by NM, 21-Jun-1993.)
@@ -26388,8 +26393,7 @@ choice between (what we call) a "definitional form" where the shorter
        7-Oct-2016.)  (Proof shortened by Wolf Lammen, 17-Nov-2019.)  Avoid
        ~ ax-13 .  (Revised by Wolf Lammen, 10-May-2023.) $)
     cleqf $p |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) $=
-      ( vy cv wcel wnfc wnf nfcr ax-mp nf5ri cleqh ) AFBCFGZBHZAABIPAJDAFBKLMOC
-      HZAACIQAJEAFCKLMN $.
+      ( vy cv wcel nfcriv nf5ri cleqh ) AFBCFGZBHAAFBDIJLCHAAFCEIJK $.
 
     $( Obsolete version of ~ cleqf as of 10-May-2023.  (Contributed by NM,
        26-May-1993.)  (Revised by Mario Carneiro, 7-Oct-2016.)  (Proof
@@ -26410,12 +26414,21 @@ choice between (what we call) a "definitional form" where the shorter
   $}
 
   ${
-    $d x y $.  $d y A $.  $d y ph $.
     abeq2f.0 $e |- F/_ x A $.
     $( Equality of a class variable and a class abstraction.  In this version,
        the fact that ` x ` is a non-free variable in ` A ` is explicitly stated
-       as a hypothesis.  (Contributed by Thierry Arnoux, 11-May-2017.) $)
+       as a hypothesis.  (Contributed by Thierry Arnoux, 11-May-2017.)  Avoid
+       ~ ax-13 .  (Revised by Wolf Lammen, 13-May-2023.) $)
     abeq2f $p |- ( A = { x | ph } <-> A. x ( x e. A <-> ph ) ) $=
+      ( cab wceq cv wcel wb wal nfab1 cleqf abid bibi2i albii bitri ) CABEZFBGZ
+      CHZRQHZIZBJSAIZBJBCQDABKLUAUBBTASABMNOP $.
+
+    $d x y $.  $d y A $.  $d y ph $.
+    $( Equality of a class variable and a class abstraction.  In this version,
+       the fact that ` x ` is a non-free variable in ` A ` is explicitly stated
+       as a hypothesis.  (Contributed by Thierry Arnoux, 11-May-2017.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    abeq2fOLD $p |- ( A = { x | ph } <-> A. x ( x e. A <-> ph ) ) $=
       ( vy cab wceq cv wcel wb wal nfcrii hbab1 cleqh abid bibi2i albii bitri )
       CABFZGBHZCIZTSIZJZBKUAAJZBKBECSBECDLABEMNUCUDBUBAUAABOPQR $.
   $}