spimv1 -> spimfv (#3604)

Author: wlammen

changes-set.txt

@@ -101,6 +101,7 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+31-Oct-23 spimv1    spimfv      labeling consistent with speimfv
 23-Oct-23 bj-alequexv alequexv  moved from BJ's mathbox to main set.mm
 23-Oct-23 axext2    axexte      existential form of ax-ext
 23-Oct-23 axext3    axextg      more general form of ax-ext

set.mm

@@ -18769,6 +18769,40 @@ Converse of the inference rule of (universal) generalization ~ ax-gen .
       ( wo wex 19.43 19.9 orbi1i bitri ) ABECFACFZBCFZEALEABCGKALACDHIJ $.
   $}
 
+  ${
+    $d x y $.
+    spimfv.nf $e |- F/ x ps $.
+    spimfv.1 $e |- ( x = y -> ( ph -> ps ) ) $.
+    $( Version of ~ spim with a disjoint variable condition, which does not
+       require ~ ax-13 .  See ~ spimvw for a version with two disjoint variable
+       conditions, requiring fewer axioms, and ~ spimv for another variant.
+       (Contributed by BJ, 31-May-2019.) $)
+    spimfv $p |- ( A. x ph -> ps ) $=
+      ( weq wi ax6ev eximii 19.36i ) ABCECDGABHCCDIFJK $.
+  $}
+
+  ${
+    $d x y $.
+    chvarfv.nf $e |- F/ x ps $.
+    chvarfv.1 $e |- ( x = y -> ( ph <-> ps ) ) $.
+    chvarfv.2 $e |- ph $.
+    $( Version of ~ chvar with a disjoint variable condition, which does not
+       require ~ ax-13 .  (Contributed by BJ, 31-May-2019.) $)
+    chvarfv $p |- ps $=
+      ( weq biimpd spimfv mpg ) ABCABCDECDHABFIJGK $.
+  $}
+
+  ${
+    $d x y $.  $d y ph $.
+    cbv3v2.nf $e |- F/ x ps $.
+    cbv3v2.1 $e |- ( x = y -> ( ph -> ps ) ) $.
+    $( Version of ~ cbv3 with two disjoint variable conditions, which does not
+       require ~ ax-11 nor ~ ax-13 .  (Contributed by BJ, 24-Jun-2019.)  (Proof
+       shortened by Wolf Lammen, 30-Aug-2021.) $)
+    cbv3v2 $p |- ( A. x ph -> A. y ps ) $=
+      ( wal spimfv alrimiv ) ACGBDABCDEFHI $.
+  $}
+
   ${
     sbimd.1 $e |- F/ x ph $.
     sbimd.2 $e |- ( ph -> ( ps -> ch ) ) $.
@@ -18961,40 +18995,6 @@ Converse of the inference rule of (universal) generalization ~ ax-gen .
   drsb2 $p |- ( A. x x = y -> ( [ x / z ] ph <-> [ y / z ] ph ) ) $=
     ( weq wsb wb sbequ sps ) BCEADBFADCFGBABCDHI $.
 
-  ${
-    $d x y $.
-    spimv1.nf $e |- F/ x ps $.
-    spimv1.1 $e |- ( x = y -> ( ph -> ps ) ) $.
-    $( Version of ~ spim with a disjoint variable condition, which does not
-       require ~ ax-13 .  See ~ spimvw for a version with two disjoint variable
-       conditions, requiring fewer axioms, and ~ spimv for another variant.
-       (Contributed by BJ, 31-May-2019.) $)
-    spimv1 $p |- ( A. x ph -> ps ) $=
-      ( weq wi ax6ev eximii 19.36i ) ABCECDGABHCCDIFJK $.
-  $}
-
-  ${
-    $d x y $.
-    chvarfv.nf $e |- F/ x ps $.
-    chvarfv.1 $e |- ( x = y -> ( ph <-> ps ) ) $.
-    chvarfv.2 $e |- ph $.
-    $( Version of ~ chvar with a disjoint variable condition, which does not
-       require ~ ax-13 .  (Contributed by BJ, 31-May-2019.) $)
-    chvarfv $p |- ps $=
-      ( weq biimpd spimv1 mpg ) ABCABCDECDHABFIJGK $.
-  $}
-
-  ${
-    $d x y $.  $d y ph $.
-    cbv3v2.nf $e |- F/ x ps $.
-    cbv3v2.1 $e |- ( x = y -> ( ph -> ps ) ) $.
-    $( Version of ~ cbv3 with two disjoint variable conditions, which does not
-       require ~ ax-11 nor ~ ax-13 .  (Contributed by BJ, 24-Jun-2019.)  (Proof
-       shortened by Wolf Lammen, 30-Aug-2021.) $)
-    cbv3v2 $p |- ( A. x ph -> A. y ps ) $=
-      ( wal spimv1 alrimiv ) ACGBDABCDEFHI $.
-  $}
-
   ${
     $d x y $.
     equsalv.nf $e |- F/ x ps $.
@@ -19792,7 +19792,7 @@ Corresponds to the dual of Axiom (B) of modal logic.  (Contributed by NM,
     $( Version of ~ cbv3 with a disjoint variable condition, which does not
        require ~ ax-13 .  (Contributed by BJ, 31-May-2019.) $)
     cbv3v $p |- ( A. x ph -> A. y ps ) $=
-      ( wal nf5ri hbal spimv1 alrimih ) ACHBDADCADEIJABCDFGKL $.
+      ( wal nf5ri hbal spimfv alrimih ) ACHBDADCADEIJABCDFGKL $.
   $}
 
   ${
@@ -20346,7 +20346,7 @@ theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10).  In the
     $d x ps $.
     spimv.1 $e |- ( x = y -> ( ph -> ps ) ) $.
     $( A version of ~ spim with a distinct variable requirement instead of a
-       bound-variable hypothesis.  See ~ spimv1 and ~ spimvw for versions
+       bound-variable hypothesis.  See ~ spimfv and ~ spimvw for versions
        requiring fewer axioms.  (Contributed by NM, 31-Jul-1993.) $)
     spimv $p |- ( A. x ph -> ps ) $=
       ( nfv spim ) ABCDBCFEG $.
@@ -527185,7 +527185,7 @@ replacing a nonfree hypothesis with a disjoint variable condition (see
   ${
     $d x y $.  $d x ps $.
     bj-spimvv.1 $e |- ( x = y -> ( ph -> ps ) ) $.
-    $( Version of ~ spimv and ~ spimv1 with a disjoint variable condition,
+    $( Version of ~ spimv and ~ spimfv with a disjoint variable condition,
        which does not require ~ ax-13 .  UPDATE: this is ~ spimvw (but
        different proof).  (Contributed by BJ, 31-May-2019.)
        (Proof modification is discouraged.) $)