shorten nfrabw (#4425)

discouraged

@@ -17882,7 +17882,6 @@ New usage of "negexsr" is discouraged (0 uses).
 New usage of "nelbOLD" is discouraged (0 uses).
 New usage of "nelbOLDOLD" is discouraged (0 uses).
 New usage of "neq0OLD" is discouraged (0 uses).
-New usage of "nf5rOLD" is discouraged (0 uses).
 New usage of "nfa1-o" is discouraged (4 uses).
 New usage of "nfaba1g" is discouraged (0 uses).
 New usage of "nfabd" is discouraged (5 uses).
@@ -17931,6 +17930,7 @@ New usage of "nfra2" is discouraged (1 uses).
 New usage of "nfra2wOLD" is discouraged (0 uses).
 New usage of "nfra2wOLDOLD" is discouraged (0 uses).
 New usage of "nfrab" is discouraged (2 uses).
+New usage of "nfrabwOLD" is discouraged (0 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).
@@ -20818,7 +20818,6 @@ Proof modification of "necon3aiOLD" is discouraged (16 steps).
 Proof modification of "nelbOLD" is discouraged (46 steps).
 Proof modification of "nelbOLDOLD" is discouraged (81 steps).
 Proof modification of "neq0OLD" is discouraged (6 steps).
-Proof modification of "nf5rOLD" is discouraged (22 steps).
 Proof modification of "nfa1-o" is discouraged (8 steps).
 Proof modification of "nfabdwOLD" is discouraged (152 steps).
 Proof modification of "nfceqdfOLD" is discouraged (48 steps).
@@ -20834,6 +20833,7 @@ Proof modification of "nfnbiOLD" is discouraged (46 steps).
 Proof modification of "nfopdALT" is discouraged (70 steps).
 Proof modification of "nfra2wOLD" is discouraged (88 steps).
 Proof modification of "nfra2wOLDOLD" is discouraged (15 steps).
+Proof modification of "nfrabwOLD" is discouraged (50 steps).
 Proof modification of "nfraldwOLD" is discouraged (41 steps).
 Proof modification of "nfreuwOLD" is discouraged (56 steps).
 Proof modification of "nfrmowOLD" is discouraged (55 steps).

set.mm

@@ -18751,13 +18751,6 @@ Converse of the inference rule of (universal) generalization ~ ax-gen .
   nf5r $p |- ( F/ x ph -> ( ph -> A. x ph ) ) $=
     ( wex wnf wal 19.8a id nfrd syl5 ) AABCABDZABEABFJABJGHI $.
 
-  $( Obsolete version of ~ nfrd as of 23-Nov-2023.  (Contributed by Mario
-     Carneiro, 26-Sep-2016.) ~ df-nf changed.  (Revised by Wolf Lammen,
-     11-Sep-2021.)  (Proof modification is discouraged.)
-     (New usage is discouraged.) $)
-  nf5rOLD $p |- ( F/ x ph -> ( ph -> A. x ph ) ) $=
-    ( wex wnf wal 19.8a wi df-nf biimpi syl5 ) AABCZABDZABEZABFLKMGABHIJ $.
-
   ${
     nf5ri.1 $e |- F/ x ph $.
     $( Consequence of the definition of not-free.  (Contributed by Mario
@@ -30632,12 +30625,21 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
     $( A variable not free in a wff remains so in a restricted class
        abstraction.  Version of ~ nfrab with a disjoint variable condition,
        which does not require ~ ax-13 .  (Contributed by NM, 13-Oct-2003.)
-       (Revised by Gino Giotto, 10-Jan-2024.) $)
+       (Revised by Gino Giotto, 10-Jan-2024.)  (Proof shortened by Wolf Lammen,
+       23-Nov-2024.) $)
     nfrabw $p |- F/_ x { y e. A | ph } $=
+      ( crab cv wcel wa cab df-rab wnfc wtru nftru wnf nfcri nfan a1i nfabdw
+      mptru nfcxfr ) BACDGCHDIZAJZCKZACDLBUEMNUDBCCOUDBPNUCABBCDFQERSTUAUB $.
+    $( $j usage 'nfrabw' avoids 'ax-13'; $)
+
+    $( Obsolete version of ~ nfrabw as of 23-Nov_2024.  (Contributed by NM,
+       13-Oct-2003.)  (Revised by Gino Giotto, 10-Jan-2024.)
+       (New usage is discouraged.)  (Proof modification is discouraged.) $)
+    nfrabwOLD $p |- F/_ x { y e. A | ph } $=
       ( crab cv wcel wa cab df-rab wnfc wtru nftru wnf nfcri a1i nfand nfabdw
       mptru nfcxfr ) BACDGCHDIZAJZCKZACDLBUEMNUDBCCONUCABUCBPNBCDFQRABPNERSTUAU
       B $.
-    $( $j usage 'nfrabw' avoids 'ax-13'; $)
+    $( $j usage 'nfrabwOLD' avoids 'ax-13'; $)
   $}
 
   ${