Skip to content

Commit

Permalink
add sb8v; rename sb8*v -> sb8*f (#4467)
Browse files Browse the repository at this point in the history 
the previous sb8v is renamed sb8f, and sb8f's corresponding sb8v is made.

sb8ev and 2sb8ev are also renamed for consistency

The rename affects comments blindly
  • Loading branch information
@icecream17
icecream17 authored Dec 9, 2024
1 parent af30a26 commit 0a3013b
Show file tree
Hide file tree
Showing 2 changed files with 61 additions and 37 deletions.
4 changes: 3 additions & 1 deletion discouraged
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18933,6 +18933,7 @@ New usage of "sb7h" is discouraged (0 uses).
New usage of "sb8" is discouraged (3 uses).
New usage of "sb8e" is discouraged (5 uses).
New usage of "sb8eu" is discouraged (3 uses).
New usage of "sb8fOLD" is discouraged (0 uses).
New usage of "sb8iota" is discouraged (0 uses).
New usage of "sb8mo" is discouraged (1 uses).
New usage of "sb9" is discouraged (1 uses).
Expand Down Expand Up @@ -19652,7 +19653,7 @@ Proof modification of "abbiOLD" is discouraged (51 steps).
Proof modification of "abfOLD" is discouraged (13 steps).
Proof modification of "abn0OLD" is discouraged (28 steps).
Proof modification of "abscncfALT" is discouraged (71 steps).
Proof modification of "abvALT" is discouraged (39 steps).
Proof modification of "abvALT" is discouraged (36 steps).
Proof modification of "ackm" is discouraged (71 steps).
Proof modification of "addltmulALT" is discouraged (497 steps).
Proof modification of "addmodlteqALT" is discouraged (237 steps).
Expand Down Expand Up @@ -21176,6 +21177,7 @@ Proof modification of "sb56OLD" is discouraged (25 steps).
Proof modification of "sb5ALT" is discouraged (80 steps).
Proof modification of "sb5ALTVD" is discouraged (110 steps).
Proof modification of "sb5OLD" is discouraged (25 steps).
Proof modification of "sb8fOLD" is discouraged (17 steps).
Proof modification of "sbabelOLD" is discouraged (126 steps).
Proof modification of "sbal1" is discouraged (149 steps).
Proof modification of "sbc2ieOLD" is discouraged (38 steps).
Expand Down
94 changes: 58 additions & 36 deletions set.mm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20329,33 +20329,55 @@ Corresponds to the dual of Axiom (B) of modal logic. (Contributed by NM,
GZEHCHRCHSEHGOQCNDEIJPTCEABDFKLRSCEKM $.
$}

${
$d ph y $. $d x y $.
$( Substitution of variable in universal quantifier. Version of ~ sb8f
with a disjoint variable condition replacing the nonfree hypothesis
` F/ y ph ` , not requiring ~ ax-12 . (Contributed by SN,
5-Dec-2024.) $)
sb8v $p |- ( A. x ph <-> A. y [ y / x ] ph ) $=
( wsb wal weq wi sb6 albii alcom equcom imbi1i equsv bitri 3bitrri ) ABCD
ZCEBCFZAGZBEZCERCEZBEABEPSCABCHIRCBJTABTCBFZAGZCEARUBCQUAABCKLIACBMNIO $.
$( $j usage 'sb8v' avoids 'ax-10' 'ax-12'; $)
$}

${
$d x y $.
sb8v.nf $e |- F/ y ph $.
sb8f.nf $e |- F/ y ph $.
$( Substitution of variable in universal quantifier. Version of ~ sb8 with
a disjoint variable condition, not requiring ~ ax-13 . (Contributed by
NM, 16-May-1993.) (Revised by Wolf Lammen, 19-Jan-2023.) $)
sb8v $p |- ( A. x ph <-> A. y [ y / x ] ph ) $=
a disjoint variable condition, not requiring ~ ax-10 or ~ ax-13 .
(Contributed by NM, 16-May-1993.) (Revised by Wolf Lammen,
19-Jan-2023.) Avoid ~ ax-10 . (Revised by SN, 5-Dec-2024.) $)
sb8f $p |- ( A. x ph <-> A. y [ y / x ] ph ) $=
( wsb wal weq wi sb6 albii alcom sbf equcom imbi1i 3bitr3ri 3bitrri ) ABC
EZCFBCGZAHZBFZCFSCFZBFABFQTCABCIJSCBKUAABACBECBGZAHZCFAUAACBIACBDLUCSCUBR
ACBMNJOJP $.
$( $j usage 'sb8f' avoids 'ax-10' 'ax-13'; $)

$( Obsolete version of ~ sb8f as of 5-Dec-2024. (Contributed by NM,
16-May-1993.) (Revised by Wolf Lammen, 19-Jan-2023.)
(Proof modification is discouraged.) (New usage is discouraged.) $)
sb8fOLD $p |- ( A. x ph <-> A. y [ y / x ] ph ) $=
( wsb nfs1v sbequ12 cbvalv1 ) AABCEBCDABCFABCGH $.

$( Substitution of variable in existential quantifier. Version of ~ sb8e
with a disjoint variable condition, not requiring ~ ax-13 .
(Contributed by NM, 12-Aug-1993.) (Revised by Wolf Lammen,
19-Jan-2023.) $)
sb8ev $p |- ( E. x ph <-> E. y [ y / x ] ph ) $=
sb8ef $p |- ( E. x ph <-> E. y [ y / x ] ph ) $=
( wsb nfs1v sbequ12 cbvexv1 ) AABCEBCDABCFABCGH $.
$}

${
$d z x $. $d z w y $.
2sb8ev.1 $e |- F/ w ph $.
2sb8ev.2 $e |- F/ z ph $.
2sb8ef.1 $e |- F/ w ph $.
2sb8ef.2 $e |- F/ z ph $.
$( An equivalent expression for double existence. Version of ~ 2sb8e with
more disjoint variable conditions, not requiring ~ ax-13 . (Contributed
by Wolf Lammen, 28-Jan-2023.) $)
2sb8ev $p |- ( E. x E. y ph <->
2sb8ef $p |- ( E. x E. y ph <->
E. z E. w [ z / x ] [ w / y ] ph ) $=
( wex wsb sb8ev exbii excom bitri nfsbv 3bitri ) ACHZBHZACEIZBHZEHZRBDIZD
( wex wsb sb8ef exbii excom bitri nfsbv 3bitri ) ACHZBHZACEIZBHZEHZRBDIZD
HZEHUAEHDHQREHZBHTPUCBACEFJKRBELMSUBERBDACEDGNJKUAEDLO $.
$}

Expand All @@ -20377,11 +20399,11 @@ Corresponds to the dual of Axiom (B) of modal logic. (Contributed by NM,
Avoid ~ ax-13 . (Revised by Wolf Lammen, 30-Jan-2023.) $)
sbnf2 $p |- ( F/ x ph
<-> A. y A. z ( [ y / x ] ph <-> [ z / x ] ph ) ) $=
( wnf wa wsb wi wal wb wex nfv sb8ev imbi12i df-nf pm11.53v 3bitr4i alcom
( wnf wa wsb wi wal wb wex nfv sb8ef imbi12i df-nf pm11.53v 3bitr4i alcom
sb8v bitri anbi12i pm4.24 2albiim ) ABEZUDFABCGZABDGZHDICIZUFUEHZDICIZFUD
UEUFJDICIUDUGUDUIABKZABIZHZUECKZUFDIZHUDUGUJUMUKUNABCACLZMABDADLZSNABOZUE
UFCDPQUDUHCIDIZUIULUFDKZUECIZHUDURUJUSUKUTABDUPMABCUOSNUQUFUEDCPQUHDCRTUA
UDUBUEUFCDUCQ $.
UEUFJDICIUDUGUDUIABKZABIZHZUECKZUFDIZHUDUGUJUMUKUNABCACLMABDSNABOZUEUFCDP
QUDUHCIDIZUIULUFDKZUECIZHUDUPUJUQUKURABDADLMABCSNUOUFUEDCPQUHDCRTUAUDUBUE
UFCDUCQ $.
$}

${
Expand All @@ -20400,7 +20422,7 @@ Corresponds to the dual of Axiom (B) of modal logic. (Contributed by NM,
2-Feb-2005.) (Proof shortened by Wolf Lammen, 30-Sep-2018.) $)
2exsb $p |- ( E. x E. y ph <->
E. z E. w A. x A. y ( ( x = z /\ y = w ) -> ph ) ) $=
( wex wsb weq wa wi wal nfv 2sb8ev 2sb6 2exbii bitri ) ACFBFACEGBDGZEFDFB
( wex wsb weq wa wi wal nfv 2sb8ef 2sb6 2exbii bitri ) ACFBFACEGBDGZEFDFB
DHCEHIAJCKBKZEFDFABCDEAELADLMQRDEABCDENOP $.
$}

Expand Down Expand Up @@ -22256,15 +22278,15 @@ that proposition with a distinct variable (inference associated with
sb8.1 $e |- F/ y ph $.
$( Substitution of variable in universal quantifier. Usage of this theorem
is discouraged because it depends on ~ ax-13 . For a version requiring
disjoint variables, but fewer axioms, see ~ sb8v . (Contributed by NM,
disjoint variables, but fewer axioms, see ~ sb8f . (Contributed by NM,
16-May-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof
shortened by Jim Kingdon, 15-Jan-2018.) (New usage is discouraged.) $)
sb8 $p |- ( A. x ph <-> A. y [ y / x ] ph ) $=
( wsb nfs1 sbequ12 cbval ) AABCEBCDABCDFABCGH $.

$( Substitution of variable in existential quantifier. Usage of this
theorem is discouraged because it depends on ~ ax-13 . For a version
requiring disjoint variables, but fewer axioms, see ~ sb8ev .
requiring disjoint variables, but fewer axioms, see ~ sb8ef .
(Contributed by NM, 12-Aug-1993.) (Revised by Mario Carneiro,
6-Oct-2016.) (Proof shortened by Jim Kingdon, 15-Jan-2018.)
(New usage is discouraged.) $)
Expand Down Expand Up @@ -22427,7 +22449,7 @@ that proposition with a distinct variable (inference associated with
$d z w ph $.
$( An equivalent expression for double existence. Usage of this theorem is
discouraged because it depends on ~ ax-13 . For a version requiring
more disjoint variables, but fewer axioms, see ~ 2sb8ev . (Contributed
more disjoint variables, but fewer axioms, see ~ 2sb8ef . (Contributed
by Wolf Lammen, 2-Nov-2019.) (New usage is discouraged.) $)
2sb8e $p |- ( E. x E. y ph <->
E. z E. w [ z / x ] [ w / y ] ph ) $=
Expand Down Expand Up @@ -22736,7 +22758,7 @@ derived from that of uniqueness ( ~ df-mo ). (Contributed by Wolf
A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) ) $=
( vz wmo wsb wa weq wal nfmo1 nfmov wex df-mo spsbim equsb3 syl6ib alrimi
wi sp anim12d equtr2 syl6 exlimiv sylbi nfs1v pm3.21 imim1d alimd aleximi
com12 sb8ev mof 3imtr4g moabs sylibr alcoms impbii ) ABFZAABCGZHZBCIZSZCJ
com12 sb8ef mof 3imtr4g moabs sylibr alcoms impbii ) ABFZAABCGZHZBCIZSZCJ
ZBJUSVDBABKUSVCCACBDLUSABEIZSZBJZEMVCABENVGVCEVGVAVECEIZHVBVGAVEUTVHVFBTV
GUTVEBCGVHAVEBCOBCEPQUABCEUBUCUDUERRVCUSCBVCBJZCJZABMZUSSUSVJUTCMAVBSZBJZ
CMVKUSVIUTVMCUTVIVMUTVCVLBABCUFUTAVAVBUTAUGUHUIUKUJABCDULABCDUMUNABUOUPUQ
Expand Down Expand Up @@ -23130,10 +23152,10 @@ of the unique existential quantifier (note that ` y ` and ` z ` need not
shortened by Wolf Lammen, 24-Aug-2019.) Factor out common proof lines.
(Revised by Wolf Lammen, 9-Feb-2023.) $)
sb8eulem $p |- ( E! x ph <-> E! y [ y / x ] ph ) $=
( vz weq wb wal wex wsb weu nfv sb8v equsb3 sblbis albii nfbi sbequ eu6
( vz weq wb wal wex wsb weu sb8v equsb3 sblbis albii nfv nfbi sbequ eu6
equequ1 bibi12d cbvalv1 3bitri exbii 3bitr4i ) ABFGZHZBIZFJABCKZCFGZHZCIZ
FJABLUJCLUIUMFUIUHBDKZDIABDKZDFGZHZDIUMUHBDUHDMNUNUQDUGUPABDBDFOPQUQULDCU
OUPCEUPCMRULDMDCGUOUJUPUKADCBSDCFUAUBUCUDUEABFTUJCFTUF $.
FJABLUJCLUIUMFUIUHBDKZDIABDKZDFGZHZDIUMUHBDMUNUQDUGUPABDBDFNOPUQULDCUOUPC
EUPCQRULDQDCGUOUJUPUKADCBSDCFUAUBUCUDUEABFTUJCFTUF $.
$}

${
Expand Down Expand Up @@ -23206,7 +23228,7 @@ of the unique existential quantifier (note that ` y ` and ` z ` need not
9-Mar-1995.) (Revised by Gino Giotto, 10-Jan-2024.)
(Proof modification is discouraged.) (New usage is discouraged.) $)
cbvmowOLD $p |- ( E* x ph <-> E* y ps ) $=
( wmo wsb wex weu wi sb8ev sb8euv imbi12i moeu 3bitr4i sbiev mobii bitri
( wmo wsb wex weu wi sb8ef sb8euv imbi12i moeu 3bitr4i sbiev mobii bitri
) ACHZACDIZDHZBDHACJZACKZLUBDJZUBDKZLUAUCUDUFUEUGACDEMACDENOACPUBDPQUBBDA
BCDFGRST $.
$( $j usage 'cbvmowOLD' avoids 'ax-13'; $)
Expand Down Expand Up @@ -23663,7 +23685,7 @@ of the unique existential quantifier (note that ` y ` and ` z ` need not
( x = z /\ y = w ) ) ) $=
( weq wa wi wal wex wsb wmo nfmo1 nfe1 nfmov nfan 19.8a spsbe sbimi nfv
2mo2 biimpi 19.21bbi syl2ani sbcom2 sylbi anim12ii alrimi alrimivv sylbir
mo3 nfs1v nfsbv pm3.21 imim1d alimd aleximi 2nexaln 2sb8ev xchnxbi pm2.21
mo3 nfs1v nfsbv pm3.21 imim1d alimd aleximi 2nexaln 2sb8ef xchnxbi pm2.21
com12 wn 2alimi 2eximi 19.23bi pm2.61d1 impbii alrot4 bitri ) ABDFZCEFZGZ
HZCIZBIZEJZDJZAACEKZBDKZGZVMHZCIZBIZEIZDIZWBEIDICIBIVRWFVRACJZBLZABJZCLZG
ZWFABCDEUAWKWDDEWKWCBWHWJBWGBMWIBCABNOPWKWBCWHWJCWGCBACNOWICMPWHWAVKWJVLA
Expand Down Expand Up @@ -31957,8 +31979,8 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is
(Proof shortened by BJ, 30-Aug-2024.) $)
abv $p |- ( { x | ph } = _V <-> A. x ph ) $=
( vy cab wtru wceq wsb wal cvv cv wcel wb dfcleq vextru tbt df-clab albii
bitr3i bitri dfv2 eqeq2i nfv sb8v 3bitr4i ) ABDZEBDZFZABCGZCHZUEIFABHUGCJ
ZUEKZUJUFKZLZCHUICUEUFMUMUHCUMUKUHULUKBCNOACBPRQSIUFUEBTUAABCACUBUCUD $.
bitr3i bitri dfv2 eqeq2i sb8v 3bitr4i ) ABDZEBDZFZABCGZCHZUDIFABHUFCJZUDK
ZUIUEKZLZCHUHCUDUEMULUGCULUJUGUKUJBCNOACBPRQSIUEUDBTUAABCUBUC $.
$( $j usage 'abv' avoids 'df-clel' 'ax-8' 'ax-13'; $)
$}

Expand All @@ -31968,8 +31990,8 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is
by BJ, 19-Mar-2021.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
abvALT $p |- ( { x | ph } = _V <-> A. x ph ) $=
( vy cv cab wcel wal wsb cvv wceq df-clab albii eqv nfv sb8v 3bitr4i ) CD
ABEZFZCGABCHZCGQIJABGRSCACBKLCQMABCACNOP $.
( vy cv cab wcel wal wsb cvv wceq df-clab albii eqv sb8v 3bitr4i ) CDABEZ
FZCGABCHZCGPIJABGQRCACBKLCPMABCNO $.
$}

${
Expand Down Expand Up @@ -471458,7 +471480,7 @@ and the expression ( x e. A /\ x e. B ) ` .
1-Mar-2017.) $)
mo5f $p |- ( E* x ph <->
A. i A. j ( ( [ i / x ] ph /\ [ j / x ] ph ) -> i = j ) ) $=
( wmo wsb wa weq wi wal mo3 nfsbv nfan nfv nfim nfal sb8v sbim sban nfs1v
( wmo wsb wa weq wi wal mo3 nfsbv nfan nfv nfim nfal sb8f sbim sban nfs1v
sbf bicomi anbi2i bitr4i equsb3 imbi12i bitri sbalv albii 3bitri ) ABGAAB
DHZIZBDJZKZDLZBLUQBCHZCLABCHZUMIZCDJZKZDLZCLABDFMUQBCUPCDUNUOCAUMCEABDCEN
OUOCPQRSURVCCUPVBBCDUPBCHUNBCHZUOBCHZKVBUNUOBCTVDUTVEVAVDUSUMBCHZIUTAUMBC
Expand Down Expand Up @@ -515389,7 +515411,7 @@ become an indirect lemma of the theorem in question (i.e. a lemma of a
requiring ~ ax-13 . (Contributed by Gino Giotto, 27-Mar-2024.)
(New usage is discouraged.) $)
bnj985v $p |- ( G e. B <-> E. p ch" ) $=
( wcel wex wsbc cvv wb bnj918 bnj984 ax-mp sbcex2 sb8ev sbsbc exbii bitri
( wcel wex wsbc cvv wb bnj918 bnj984 ax-mp sbcex2 sb8ef sbsbc exbii bitri
cv wsb nfv bnj133 sbcbii 3bitr4i ) IDRZCHSZGITZLJSZIUARUQUSUBEGHIQUCABCUA
DFGHIMPUDUEKJSZGITKGITZJSUSUTKJGIUFURVAGIURCHJUKTZKJURCHJULZJSVCJSCHJCJUM
UGVDVCJCHJUHUIUJNUNUOLVBJOUIUPUJ $.
Expand Down Expand Up @@ -552353,7 +552375,7 @@ two more essential steps but fewer total steps (since there are fewer

$( Goal: closed form of sb8, but first need closed form of cbval.
Remark: The equality may be a hypothesis.
TODO: prove sb8v with fewer axioms than ~ sb8 ; use it for ~ abtrubi . $)
TODO: prove sb8f with fewer axioms than ~ sb8 ; use it for ~ abtrubi . $)


$(
Expand Down Expand Up @@ -552901,7 +552923,7 @@ References are made to the second edition (1927, reprinted 1963) of
by BJ, 15-Sep-2018.) (Proof modification is discouraged.) $)
ax11-pm2 $p |- ( A. x A. y ph -> A. y A. x ph ) $=
( vt vz wal wsb wi 2stdpc4 gen2 nfv nfal 2stdpc5 ax-mp nfsbv albii sylibr
sb8v sbal ) ACFZBFZABFZCDGZDFZUBCFUAACDGZBFZDFZUDUAUEBEGZEFZDFZUGUAUHHZEF
sb8f sbal ) ACFZBFZABFZCDGZDFZUBCFUAACDGZBFZDFZUDUAUEBEGZEFZDFZUGUAUHHZEF
DFUAUJHUKDEABCEDIJUAUHDETDBADCADKZLLTEBAECAEKZLLMNUFUIDUEBEACDEUMORPQUCUF
DABCDSPQUBCDADBULLRQ $.
$}
Expand Down Expand Up @@ -554152,7 +554174,7 @@ nonfreeness hypothesis (for the sake of illustration). (Contributed by
$( Version of ~ df-nfc with a disjoint variable condition replaced with a
nonfreeness hypothesis. (Contributed by BJ, 2-May-2019.) $)
bj-nfcf $p |- ( F/_ x A <-> A. y F/ x y e. A ) $=
( vz wnfc wcel wnf wal df-nfc nfcri nfnf sb8v bj-sbnf clelsb1 nfbii bitri
( vz wnfc wcel wnf wal df-nfc nfcri nfnf sb8f bj-sbnf clelsb1 nfbii bitri
cv wsb albii ) ACFERCGZAHZEIZBRCGZAHZBIZAECJUCUBEBSZBIUFUBEBUABABECDKLMUG
UEBUGUAEBSZAHUEUAAEBNUHUDAEBCOPQTQQ $.
$}
Expand Down Expand Up @@ -579513,9 +579535,9 @@ the next (since the empty set has a finite subcover, the
explicit nonfree variable condition. (Contributed by Giovanni
Mascellani, 29-May-2019.) $)
sbcalf $p |- ( [. A / x ]. A. y ph <-> A. y [. A / x ]. ph ) $=
( vz wal wsbc wsb nfv sb8v sbcbii sbcal nfs1v nfsbcw weq sbequ12r sbcbidv
cbvalv1 3bitri ) ACGZBDHACFIZFGZBDHUBBDHZFGABDHZCGUAUCBDACFAFJKLUBFBDMUDU
EFCUBCBDEACFNOUEFJFCPUBABDAFCQRST $.
( vz wal wsbc wsb sb8v sbcbii sbcal nfs1v nfsbcw nfv weq sbequ12r sbcbidv
cbvalv1 3bitri ) ACGZBDHACFIZFGZBDHUBBDHZFGABDHZCGUAUCBDACFJKUBFBDLUDUEFC
UBCBDEACFMNUEFOFCPUBABDAFCQRST $.
$}

${
Expand All @@ -579525,7 +579547,7 @@ the next (since the empty set has a finite subcover, the
explicit nonfree variable condition. (Contributed by Giovanni
Mascellani, 29-May-2019.) $)
sbcexf $p |- ( [. A / x ]. E. y ph <-> E. y [. A / x ]. ph ) $=
( vz wex wsbc wsb nfv sb8ev sbcbii sbcex2 nfsbcw sbequ12r sbcbidv cbvexv1
( vz wex wsbc wsb nfv sb8ef sbcbii sbcex2 nfsbcw sbequ12r sbcbidv cbvexv1
nfs1v weq 3bitri ) ACGZBDHACFIZFGZBDHUBBDHZFGABDHZCGUAUCBDACFAFJKLUBFBDMU
DUEFCUBCBDEACFRNUEFJFCSUBABDAFCOPQT $.
$}
Expand Down

0 comments on commit 0a3013b

Please sign in to comment.