Move to Main ~nsb ~sbn1. Shorten ~noel. Shorten and axiom-reduce ~bj-…

…ab0. (metamath#4225)

discouraged

@@ -17474,6 +17474,7 @@ New usage of "nnadjuALT" is discouraged (0 uses).
 New usage of "nnexALT" is discouraged (3 uses).
 New usage of "nnindALT" is discouraged (0 uses).
 New usage of "nnne0ALT" is discouraged (0 uses).
+New usage of "noelOLD" is discouraged (0 uses).
 New usage of "nonbooli" is discouraged (0 uses).
 New usage of "noranOLD" is discouraged (0 uses).
 New usage of "norassOLD" is discouraged (0 uses).
@@ -18273,6 +18274,7 @@ New usage of "sbie" is discouraged (19 uses).
 New usage of "sbied" is discouraged (3 uses).
 New usage of "sbiedv" is discouraged (1 uses).
 New usage of "sbiedwOLD" is discouraged (0 uses).
+New usage of "sbn1ALT" is discouraged (0 uses).
 New usage of "sbtALT" is discouraged (0 uses).
 New usage of "sbtT" is discouraged (0 uses).
 New usage of "sbtr" is discouraged (0 uses).
@@ -18977,7 +18979,7 @@ Proof modification of "bj-19.12" is discouraged (35 steps).
 Proof modification of "bj-19.21t0" is discouraged (39 steps).
 Proof modification of "bj-19.41al" is discouraged (51 steps).
 Proof modification of "bj-a1k" is discouraged (10 steps).
-Proof modification of "bj-ab0" is discouraged (54 steps).
+Proof modification of "bj-ab0" is discouraged (39 steps).
 Proof modification of "bj-abf" is discouraged (13 steps).
 Proof modification of "bj-ablsscmn" is discouraged (10 steps).
 Proof modification of "bj-ablsscmnel" is discouraged (5 steps).
@@ -19997,6 +19999,7 @@ Proof modification of "nnadjuALT" is discouraged (62 steps).
 Proof modification of "nnexALT" is discouraged (34 steps).
 Proof modification of "nnindALT" is discouraged (15 steps).
 Proof modification of "nnne0ALT" is discouraged (19 steps).
+Proof modification of "noelOLD" is discouraged (77 steps).
 Proof modification of "noranOLD" is discouraged (63 steps).
 Proof modification of "norassOLD" is discouraged (276 steps).
 Proof modification of "norcomOLD" is discouraged (27 steps).
@@ -20198,6 +20201,7 @@ Proof modification of "sbcrexgOLD" is discouraged (77 steps).
 Proof modification of "sbcssgVD" is discouraged (229 steps).
 Proof modification of "sbequ2OLD" is discouraged (75 steps).
 Proof modification of "sbiedwOLD" is discouraged (51 steps).
+Proof modification of "sbn1ALT" is discouraged (41 steps).
 Proof modification of "sbsbc" is discouraged (21 steps).
 Proof modification of "sbtALT" is discouraged (12 steps).
 Proof modification of "sbtT" is discouraged (7 steps).

set.mm

@@ -17771,6 +17771,17 @@ disjoint variable condition ( ~ sb2 ).  Theorem ~ sb6f replaces the
       ( weq wsb equid equsb3 mpbir ) ABCABDBBCBEABBFG $.
   $}
 
+  $( Any substitution in an always false formula is false.  (Contributed by
+     Steven Nguyen, 3-May-2023.) $)
+  nsb $p |- ( A. x -. ph -> -. [ t / x ] ph ) $=
+    ( wn wal wex wsb alnex biimpi spsbe nsyl ) ADBEZABFZABCGLMDABHIABCJK $.
+
+  $( One direction of ~ sbn , using fewer axioms.  Compare ~ 19.2 .
+     (Contributed by Steven Nguyen, 18-Aug-2023.) $)
+  sbn1 $p |- ( [ t / x ] -. ph -> -. [ t / x ] ph ) $=
+    ( wn wsb wfal nsb fal mpg pm2.21 sb2imi mtoi ) ADZBCEABCEFBCEZFDNDBFBCGHIMA
+    FBCAFJKL $.
+
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -39481,12 +39492,21 @@ among classes ( ~ eq0 , as opposed to the weaker uniqueness among sets,
   $( $j usage 'dfnul4' avoids 'df-clel' 'ax-8'; $)
 
   ${
-    $d A x $.
+    $d A x y $.
     $( The empty set has no elements.  Theorem 6.14 of [Quine] p. 44.
        (Contributed by NM, 21-Jun-1993.)  (Proof shortened by Mario Carneiro,
        1-Sep-2015.)  Remove dependency on ~ ax-10 , ~ ax-11 , and ~ ax-12 .
-       (Revised by Steven Nguyen, 3-May-2023.) $)
+       (Revised by Steven Nguyen, 3-May-2023.)  (Proof shortened by BJ,
+       18-Sep-2024.) $)
     noel $p |- -. A e. (/) $=
+      ( vx vy c0 wcel cv wceq wa wex wfal wsb wn fal sbt sbn1 cab dfnul4 eleq2i
+      ax-mp mtbir df-clab bitri intnan nex dfclel ) ADEBFZAGZUFDEZHZBIUIBUHUGUH
+      JCBKZJLZCBKUJLUKCBMNJCBOSUHUFJCPZEUJDULUFCQRJBCUAUBTUCUDBADUET $.
+
+    $( Obsolete version of ~ noel as of 18-Sep-2024.  (Contributed by NM,
+       21-Jun-1993.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    noelOLD $p |- -. A e. (/) $=
       ( vx vy c0 wcel cv wceq wa wex cvv cab pm3.24 nex wsb df-clab spsbe sylbi
       wn mto mtbir cdif df-nul df-dif eqtri eleq2i intnan dfclel ) ADEBFZAGZUHD
       EZHZBIUKBUJUIUJUHCFJEZULRHZCKZEZUOUMCIZUMCULLMUOUMCBNUPUMBCOUMCBPQSDUNUHD
@@ -547136,6 +547156,13 @@ References are made to the second edition (1927, reprinted 1963) of
       JCQHZDIZFJBDKCDKASUAFARTDABCQELMNBDFOCDFOP $.
   $}
 
+  $( Alternate proof of ~ sbn1 , not using the false constant.  (Contributed by
+     BJ, 18-Sep-2024.)  (Proof modification is discouraged.)
+     (New usage is discouraged.) $)
+  sbn1ALT $p |- ( [ t / x ] -. ph -> -. [ t / x ] ph ) $=
+    ( wn wsb wa nsb pm3.24 mpg sban mtbi pm3.21 mtoi ) ADZBCEZABCEZPOFZANFZBCEZ
+    QRDSDBRBCGAHIANBCJKOPLM $.
+
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -547875,9 +547902,8 @@ but the latter requires a domain with at least two objects (hence uses
        ~ abf ).  (Contributed by BJ, 24-Jul-2019.)
        (Proof modification is discouraged.) $)
     bj-ab0 $p |- ( A. x -. ph -> { x | ph } = (/) ) $=
-      ( vy wn wal cv cab wcel c0 wceq ax-5 wsb stdpc4 sbn sylib df-clab sylnibr
-      alrimih eq0 sylibr ) ADZBEZCFABGZHZDZCEUCIJUBUECUBCKUBABCLZUDUBUABCLUFDUA
-      BCMABCNOACBPQRCUCST $.
+      ( vy wn wal cab wsb cv wcel stdpc4 sbn1 syl df-clab sylnibr eq0rdv ) ADZB
+      EZCABFZQABCGZCHRIQPBCGSDPBCJABCKLACBMNO $.
   $}
 
   ${
@@ -645870,14 +645896,6 @@ D Fn ( I ... ( M - 1 ) ) /\
       ( id syl3an ) ABCDEEFGHEJIK $.
   $}
 
-  ${
-    nsb.1 $e |- -. ph $.
-    $( Generalization rule for negated wff.  (Contributed by Steven Nguyen,
-       3-May-2023.) $)
-    nsb $p |- -. [ x / y ] ph $=
-      ( wsb wex nex spsbe mto ) ACBEACFACDGACBHI $.
-  $}
-
   ${
     $d x ph $.
     sbtd.1 $e |- ( ph -> ps ) $.
@@ -645887,11 +645905,6 @@ D Fn ( I ... ( M - 1 ) ) /\
       ( wal wsb alrimiv stdpc4 syl ) ABCFBCDGABCEHBCDIJ $.
   $}
 
-  $( One direction of ~ sbn , using fewer axioms.  Compare ~ 19.2 .
-     (Contributed by Steven Nguyen, 18-Aug-2023.) $)
-  sbn1 $p |- ( [ t / x ] -. ph -> -. [ t / x ] ph ) $=
-    ( wn wsb wfal fal nsb pm2.21 sb2imi mtoi ) ADZBCEABCEFBCEFCBGHLAFBCAFIJK $.
-
   $( One direction of ~ sbor , using fewer axioms.  Compare ~ 19.33 .
      (Contributed by Steven Nguyen, 18-Aug-2023.) $)
   sbor2 $p |- ( ( [ t / x ] ph \/ [ t / x ] ps ) -> [ t / x ] ( ph \/ ps ) ) $=