move bj-spvv to main (as spvv) (#3276)

* move bj-spvv to main (as spvv)

spvw already exists

auto use spvv in place of spv and bj-spvv
in both cases they were noted in bj's mathbox, so add tags to clarify origin

update bj-ru0 now that + spvv and - ax-13

nalset is quite related to ru, through ruv vprc

* ru $j [+ax-13]

Author: icecream17

changes-set.txt

@@ -27,6 +27,8 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+ 1-Jul-23 bj-nalset nalset      moved from BJ's mathbox to main set.mm
+ 1-Jul-23 bj-spvv   spvv        moved from BJ's mathbox to main set.mm
 25-Jun-23 2reu4     [same]      moved from AV's mathbox to main set.mm
 25-Jun-23 2reu4a    [same]      moved from AV's mathbox to main set.mm
 25-Jun-23 2reu2     [same]      moved from AV's mathbox to main set.mm

discouraged

@@ -18390,7 +18390,6 @@ Proof modification of "bj-issetw" is discouraged (21 steps).
 Proof modification of "bj-issetwt" is discouraged (63 steps).
 Proof modification of "bj-mo3OLD" is discouraged (206 steps).
 Proof modification of "bj-mpt2mptALT" is discouraged (130 steps).
-Proof modification of "bj-nalset" is discouraged (100 steps).
 Proof modification of "bj-ndxarg" is discouraged (37 steps).
 Proof modification of "bj-ndxid" is discouraged (28 steps).
 Proof modification of "bj-nfab1" is discouraged (10 steps).
@@ -18435,7 +18434,6 @@ Proof modification of "bj-spimev" is discouraged (19 steps).
 Proof modification of "bj-spimevv" is discouraged (9 steps).
 Proof modification of "bj-spimtv" is discouraged (52 steps).
 Proof modification of "bj-spimvv" is discouraged (16 steps).
-Proof modification of "bj-spvv" is discouraged (12 steps).
 Proof modification of "bj-ssbid1ALT" is discouraged (42 steps).
 Proof modification of "bj-ssbid2ALT" is discouraged (84 steps).
 Proof modification of "bj-stdpc5" is discouraged (20 steps).

set.mm

@@ -16123,6 +16123,16 @@ modal logic (the other standard formulation being ~ extru ).  Note:  This
       ( wn ax-5 spimw ) ABCDBFCGEH $.
   $}
 
+  ${
+    $d x y $.  $d x ps $.
+    spvv.1 $e |- ( x = y -> ( ph <-> ps ) ) $.
+    $( Version of ~ spv with a disjoint variable condition, which does not
+       require ~ ax-7 , ~ ax-12 , ~ ax-13 .  (Contributed by BJ,
+       31-May-2019.) $)
+    spvv $p |- ( A. x ph -> ps ) $=
+      ( weq biimpd spimvw ) ABCDCDFABEGH $.
+  $}
+
   ${
     $d x y $.  $d y ph $.
     spnfw.1 $e |- ( -. ph -> A. x -. ph ) $.
@@ -17620,7 +17630,8 @@ This axiom scheme is logically redundant (see ~ ax12w ) but is used as an
 
      It appears that this scheme cannot be derived directly from Tarski's
      axioms without auxiliary axiom scheme ~ ax-12 .  It is thought the best we
-     can do using only Tarski's axioms is ~ spw .  (Contributed by NM,
+     can do using only Tarski's axioms is ~ spw .  Also see ~ spvw where ` x `
+     and ` ph ` are distinct, using fewer axioms.  (Contributed by NM,
      21-May-2008.)  (Proof shortened by Scott Fenton, 24-Jan-2011.)  (Proof
      shortened by Wolf Lammen, 13-Jan-2018.) $)
   sp $p |- ( A. x ph -> ph ) $=
@@ -19415,8 +19426,8 @@ theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10).  In the
   ${
     $d x ps $.
     spv.1 $e |- ( x = y -> ( ph <-> ps ) ) $.
-    $( Specialization, using implicit substitution.  (Contributed by NM,
-       30-Aug-1993.) $)
+    $( Specialization, using implicit substitution.  See ~ spvv for a version
+       using fewer axioms.  (Contributed by NM, 30-Aug-1993.) $)
     spv $p |- ( A. x ph -> ps ) $=
       ( weq biimpd spimv ) ABCDCDFABEGH $.
   $}
@@ -32679,13 +32690,14 @@ his New Foundations set theory (axiom system NF of [Quine] p. 331).  In
        ~ elirrv (derived from the Axiom of Regularity), so for us the Russell
        class equals the universe ` _V ` (theorem ~ ruv ).  See ~ ruALT for an
        alternate proof of ~ ru derived from that fact.  (Contributed by NM,
-       7-Aug-1994.)  (Proof modification is discouraged.) $)
+       7-Aug-1994.)  Remove use of ~ ax-13 .  (Revised by BJ, 12-Oct-2019.)
+       (Proof modification is discouraged.) $)
     ru $p |- { x | x e/ x } e/ _V $=
       ( vy cv wnel cab cvv wcel wceq wex wel wb wn pm5.19 eleq1w df-nel eleq12d
-      wal id notbid mtbir syl5bb bibi12d spv mto abeq2 nex isset nelir ) ACZUID
-      ZAEZFUKFGBCZUKHZBIUMBUMABJZUJKZAQZUPBBJZUQLZKZUQMUOUSABUIULHZUNUQUJURABUL
-      NUJAAJZLUTURUIUIOUTVAUQUTUIULUIULUTRZVBPSUAUBUCUDUJAULUETUFBUKUGTUH $.
-    $( $j usage 'ru' avoids 'ax-reg'; $)
+      wal id notbid mtbir syl5bb bibi12d spvv mto abeq2 nex isset nelir ) ACZUI
+      DZAEZFUKFGBCZUKHZBIUMBUMABJZUJKZAQZUPBBJZUQLZKZUQMUOUSABUIULHZUNUQUJURABU
+      LNUJAAJZLUTURUIUIOUTVAUQUTUIULUIULUTRZVBPSUAUBUCUDUJAULUETUFBUKUGTUH $.
+    $( $j usage 'ru' avoids 'ax-13' 'ax-reg'; $)
   $}
 
 
@@ -45437,12 +45449,14 @@ holding in an empty domain (see Axiom A5 and Rule R2 of [LeBlanc]
   ${
     $d x y z $.
     $( No set contains all sets.  Theorem 41 of [Suppes] p. 30.  (Contributed
-       by NM, 23-Aug-1993.) $)
+       by NM, 23-Aug-1993.)  Remove use of ~ ax-12 and ~ ax-13 .  (Revised by
+       BJ, 31-May-2019.) $)
     nalset $p |- -. E. x A. y y e. x $=
       ( vz wel wn wex wal alexn wa wb ax-sep elequ1 elequ2 bitrd notbid anbi12d
-      weq bibi12d spv pclem6 syl eximii mpgbi ) BADZEZBFUDBGAFEAUDABHCBDZCADZCC
-      DZEZIZJZCGZUEBUICBAKULBBDZUDUMEZIZJZUEUKUPCBCBQZUFUMUJUOCBBLUQUGUDUIUNCBA
-      LUQUHUMUQUHBCDUMCBCLCBBMNOPRSUMUDTUAUBUC $.
+      weq bibi12d spvv pclem6 syl eximii mpgbi ) BADZEZBFUDBGAFEAUDABHCBDZCADZC
+      CDZEZIZJZCGZUEBUICBAKULBBDZUDUMEZIZJZUEUKUPCBCBQZUFUMUJUOCBBLUQUGUDUIUNCB
+      ALUQUHUMUQUHBCDUMCBCLCBBMNOPRSUMUDTUAUBUC $.
+    $( $j usage 'nalset' avoids 'ax-12' 'ax-13'; $)
   $}
 
   ${
@@ -522862,16 +522876,6 @@ may also add the (partially) unbundled versions which dipense with ~ ax-13 ,
       ( nfv bj-spimev ) ABCDACFEG $.
   $}
 
-  ${
-    $d x y $.  $d x ps $.
-    bj-spvv.1 $e |- ( x = y -> ( ph <-> ps ) ) $.
-    $( Version of ~ spv with a disjoint variable condition, which does not
-       require ~ ax-7 , ~ ax-12 , ~ ax-13 .  (Contributed by BJ, 31-May-2019.)
-       (Proof modification is discouraged.) $)
-    bj-spvv $p |- ( A. x ph -> ps ) $=
-      ( weq biimpd spimvw ) ABCDCDFABEGH $.
-  $}
-
   ${
     $d x y $.
     bj-speiv.1 $e |- ( x = y -> ( ph <-> ps ) ) $.
@@ -522903,7 +522907,7 @@ may also add the (partially) unbundled versions which dipense with ~ ax-13 ,
        require ~ ax-13 .  (Contributed by BJ, 31-May-2019.)
        (Proof modification is discouraged.) $)
     bj-chvarvv $p |- ps $=
-      ( bj-spvv mpg ) ABCABCDEGFH $.
+      ( spvv mpg ) ABCABCDEGFH $.
   $}
 
   ${
@@ -523506,18 +523510,6 @@ at least two objects (see ~ bj-dtru ).  (Contributed by BJ,
       UQVBULUQUNUMAHZHZEIVBVJUPEUNUMAUCTVIVBEBUNUMVAAEBDUDUEUFUGUHUITUK $.
   $}
 
-  ${
-    $d x y z $.
-    $( Remove dependency on ~ ax-12 and ~ ax-13 (and ~ df-nf ) from ~ nalset .
-       (Contributed by BJ, 31-May-2019.)
-       (Proof modification is discouraged.) $)
-    bj-nalset $p |- -. E. x A. y y e. x $=
-      ( vz wel wn wex wal alexn wa wb ax-sep elequ1 elequ2 bitrd notbid anbi12d
-      weq bibi12d bj-spvv pclem6 syl eximii mpgbi ) BADZEZBFUDBGAFEAUDABHCBDZCA
-      DZCCDZEZIZJZCGZUEBUICBAKULBBDZUDUMEZIZJZUEUKUPCBCBQZUFUMUJUOCBBLUQUGUDUIU
-      NCBALUQUHUMUQUHBCDUMCBCLCBBMNOPRSUMUDTUAUBUC $.
-  $}
-
   ${
     $d x y z $.
     $( Remove dependency on ~ ax-13 from ~ el .  (Contributed by BJ,
@@ -525342,14 +525334,13 @@ FOL part ( ~ bj-ru0 ) and then two versions ( ~ bj-ru1 and ~ bj-ru ).
   ${
     $d x y $.
     $( The FOL part of Russell's paradox ~ ru (see also ~ bj-ru1 , ~ bj-ru ).
-       Use of ~ elequ1 , ~ bj-elequ12 , ~ bj-spvv (instead of ~ eleq1 ,
-       ~ eleq12d , ~ spv as in ~ ru ) permits to remove dependency on ~ ax-10 ,
-       ~ ax-11 , ~ ax-12 , ~ ax-13 , ~ ax-ext , ~ df-sb , ~ df-clab ,
-       ~ df-cleq , ~ df-clel .  (Contributed by BJ, 12-Oct-2019.)
-       (Proof modification is discouraged.) $)
+       Use of ~ elequ1 , ~ bj-elequ12 (instead of ~ eleq1 , ~ eleq12d as in
+       ~ ru ) permits to remove dependency on ~ ax-10 , ~ ax-11 , ~ ax-12 ,
+       ~ ax-ext , ~ df-sb , ~ df-clab , ~ df-cleq , ~ df-clel .  (Contributed
+       by BJ, 12-Oct-2019.)  (Proof modification is discouraged.) $)
     bj-ru0 $p |- -. A. x ( x e. y <-> -. x e. x ) $=
-      ( wel wal pm5.19 weq elequ1 bj-elequ12 anidms notbid bibi12d bj-spvv mto
-      wn wb ) ABCZAACZNZOZADBBCZTNZOZTESUBABABFZPTRUAABBGUCQTUCQTOABABHIJKLM $.
+      ( wel wn wal pm5.19 weq elequ1 bj-elequ12 anidms notbid bibi12d spvv mto
+      wb ) ABCZAACZDZOZAEBBCZTDZOZTFSUBABABGZPTRUAABBHUCQTUCQTOABABIJKLMN $.
   $}
 
   ${