prove nfraldw and nfra2w with fewer axioms (#4240)

discouraged

@@ -17350,9 +17350,11 @@ New usage of "nfmod2" is discouraged (5 uses).
 New usage of "nfnae" is discouraged (43 uses).
 New usage of "nfopdALT" is discouraged (0 uses).
 New usage of "nfra2" is discouraged (1 uses).
+New usage of "nfra2wOLD" is discouraged (0 uses).
 New usage of "nfrab" is discouraged (2 uses).
 New usage of "nfral" is discouraged (5 uses).
 New usage of "nfrald" is discouraged (2 uses).
+New usage of "nfraldwOLD" is discouraged (0 uses).
 New usage of "nfreu" is discouraged (0 uses).
 New usage of "nfreud" is discouraged (1 uses).
 New usage of "nfrexdg" is discouraged (2 uses).
@@ -20008,6 +20010,8 @@ Proof modification of "nfcriiOLD" is discouraged (40 steps).
 Proof modification of "nfequid-o" is discouraged (8 steps).
 Proof modification of "nfeu1ALT" is discouraged (25 steps).
 Proof modification of "nfopdALT" is discouraged (70 steps).
+Proof modification of "nfra2wOLD" is discouraged (15 steps).
+Proof modification of "nfraldwOLD" is discouraged (41 steps).
 Proof modification of "nfsbOLD" is discouraged (23 steps).
 Proof modification of "nfsumOLD" is discouraged (216 steps).
 Proof modification of "nfunidALT" is discouraged (33 steps).

set.mm

@@ -26775,8 +26775,8 @@ generally appear in a single form (either definitional, but more often
   ${
     $d x y z $.  $d z A $.
     $( Consequence of the not-free predicate.  (Contributed by Mario Carneiro,
-       11-Aug-2016.)  Drop ~ ax-12 but use ~ ax-8 , and avoid a DV condition on
-       ` y ` , ` A ` .  (Revised by SN, 3-Jun-2024.) $)
+       11-Aug-2016.)  Drop ~ ax-12 but use ~ ax-8 , ~ df-clel , and avoid a DV
+       condition on ` y ` , ` A ` .  (Revised by SN, 3-Jun-2024.) $)
     nfcr $p |- ( F/_ x A -> F/ x y e. A ) $=
       ( vz wnfc cv wcel wnf wal df-nfc weq eleq1w nfbidv spvv sylbi ) ACEDFCGZA
       HZDIBFCGZAHZADCJQSDBDBKPRADBCLMNO $.
@@ -26790,7 +26790,7 @@ generally appear in a single form (either definitional, but more often
        (New usage is discouraged.)  (Proof modification is discouraged.) $)
     nfcrALT $p |- ( F/_ x A -> F/ x y e. A ) $=
       ( wnfc cv wcel wnf wal df-nfc sp sylbi ) ACDBECFAGZBHLABCILBJK $.
-    $( $j usage 'nfcrALT' avoids 'ax-8'; $)
+    $( $j usage 'nfcrALT' avoids 'ax-8' 'df-clel'; $)
   $}
 
   ${
@@ -26816,7 +26816,7 @@ generally appear in a single form (either definitional, but more often
   $}
 
   ${
-    $d x y $.  $d y A $.
+    $d x y $.
     nfcrd.1 $e |- ( ph -> F/_ x A ) $.
     $( Consequence of the not-free predicate.  (Contributed by Mario Carneiro,
        11-Aug-2016.) $)
@@ -28942,11 +28942,19 @@ generally appear in a single form (either definitional, but more often
     nfraldw.3 $e |- ( ph -> F/ x ps ) $.
     $( Deduction version of ~ nfralw .  Version of ~ nfrald with a disjoint
        variable condition, which does not require ~ ax-13 .  (Contributed by
-       NM, 15-Feb-2013.)  (Revised by Gino Giotto, 10-Jan-2024.) $)
+       NM, 15-Feb-2013.)  (Revised by Gino Giotto, 24-Sep-2024.) $)
     nfraldw $p |- ( ph -> F/ x A. y e. A ps ) $=
+      ( wral cv wcel wi wal df-ral nfcrd nfimd nfald nfxfrd ) BDEIDJEKZBLZDMACB
+      DENATCDFASBCACDEGOHPQR $.
+    $( $j usage 'nfraldw' avoids 'ax-13' 'ax-9' 'df-cleq' 'ax-ext'; $)
+
+    $( Obsolete version of ~ nfraldw as of 24-Sep-2024.  (Contributed by NM,
+       15-Feb-2013.)  (Revised by Gino Giotto, 10-Jan-2024.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    nfraldwOLD $p |- ( ph -> F/ x A. y e. A ps ) $=
       ( wral cv wcel wi wal df-ral nfcvd nfeld nfimd nfald nfxfrd ) BDEIDJZEKZB
       LZDMACBDENAUBCDFAUABCACTEACTOGPHQRS $.
-    $( $j usage 'nfraldw' avoids 'ax-13'; $)
+    $( $j usage 'nfraldwOLD' avoids 'ax-13'; $)
   $}
 
   ${
@@ -28995,10 +29003,20 @@ generally appear in a single form (either definitional, but more often
        antecedent is restricted.  Derived automatically from ~ hbra2VD .
        Version of ~ nfra2 with a disjoint variable condition, which does not
        require ~ ax-13 .  (Contributed by Alan Sare, 31-Dec-2011.)  (Revised by
-       Gino Giotto, 10-Jan-2024.) $)
+       Gino Giotto, 24-Sep-2024.) $)
     nfra2w $p |- F/ y A. x e. A A. y e. B ph $=
+      ( wral cv wcel wi wal df-ral imbi2i albii bitri wnf nfa1 alcom nfbii mpbi
+      19.21v nfxfr ) ACEFZBDFZBGDHZCGEHAIZCJZIZBJZCUCUDUBIZBJUHUBBDKUIUGBUBUFUD
+      ACEKLMNUDUEIZBJZCJZCOUHCOUKCPULUHCULUJCJZBJUHUJCBQUMUGBUDUECTMNRSUA $.
+    $( $j usage 'nfra2w' avoids 'ax-6' 'ax-7' 'ax-8' 'df-clel' 'ax-9' 'df-cleq'
+       'ax-12' 'ax-13' 'ax-ext'; $)
+
+    $( Obsolete version of ~ nfra2w as of 24-Sep-2024.  (Contributed by Alan
+       Sare, 31-Dec-2011.)  (Revised by Gino Giotto, 10-Jan-2024.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    nfra2wOLD $p |- F/ y A. x e. A A. y e. B ph $=
       ( wral nfcv nfra1 nfralw ) ACEFCBDCDGACEHI $.
-    $( $j usage 'nfra2w' avoids 'ax-13'; $)
+    $( $j usage 'nfra2wOLD' avoids 'ax-13'; $)
   $}
 
   ${