Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sp | Structured version Visualization version Unicode version |
Description: Specialization. A
universally quantified wff implies the wff without a
quantifier Axiom scheme B5 of [Tarski] p.
67 (under his system S2, defined
in the last paragraph on p. 77). Also appears as Axiom scheme C5' in
[Megill] p. 448 (p. 16 of the preprint).
This corresponds to the axiom
(T) of modal logic.
For the axiom of specialization presented in many logic textbooks, see theorem stdpc4 2353. This theorem shows that our obsolete axiom ax-c5 34168 can be derived from the others. The proof uses ideas from the proof of Lemma 21 of [Monk2] p. 114. It appears that this scheme cannot be derived directly from Tarski's axioms without auxiliary axiom scheme ax-12 2047. It is thought the best we can do using only Tarski's axioms is spw 1967. (Contributed by NM, 21-May-2008.) (Proof shortened by Scott Fenton, 24-Jan-2011.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) |
Ref | Expression |
---|---|
sp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alex 1753 | . 2 | |
2 | 19.8a 2052 | . . 3 | |
3 | 2 | con1i 144 | . 2 |
4 | 1, 3 | sylbi 207 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wal 1481 wex 1704 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-12 2047 |
This theorem depends on definitions: df-bi 197 df-ex 1705 |
This theorem is referenced by: spi 2054 sps 2055 2sp 2056 spsd 2057 19.21bi 2059 19.3 2069 19.9d 2070 axc4 2130 axc7 2132 axc7e 2133 axc16gb 2136 sb56 2150 19.12 2164 nfaldOLD 2166 nfrOLD 2188 19.3OLD 2202 ax12 2304 ax13ALT 2305 hbae 2315 ax12OLD 2341 ax12b 2345 sb2 2352 dfsb2 2373 sbequi 2375 nfsb4t 2389 exsb 2468 mo3 2507 mopick 2535 axi4 2593 axi5r 2594 nfcr 2756 rsp 2929 ceqex 3333 elrab3t 3362 abidnf 3375 mob2 3386 sbcnestgf 3995 mpteq12f 4731 axrep2 4773 axnulALT 4787 dtru 4857 eusv1 4860 alxfr 4878 iota1 5865 dffv2 6271 fiint 8237 isf32lem9 9183 nd3 9411 axrepnd 9416 axpowndlem2 9420 axpowndlem3 9421 axacndlem4 9432 trclfvcotr 13750 relexpindlem 13803 fiinopn 20706 ex-natded9.26-2 27277 bnj1294 30888 bnj570 30975 bnj953 31009 bnj1204 31080 bnj1388 31101 frmin 31739 bj-hbxfrbi 32608 bj-ssbft 32642 bj-ssbequ2 32643 bj-ssbid2ALT 32646 bj-sb 32677 bj-spst 32679 bj-19.21bit 32680 bj-19.3t 32689 bj-sb2v 32753 bj-axrep2 32789 bj-dtru 32797 bj-hbaeb2 32805 bj-hbnaeb 32807 bj-sbsb 32824 bj-nfcsym 32886 exlimim 33189 exellim 33192 wl-aleq 33322 wl-equsal1i 33329 wl-sb8t 33333 wl-lem-exsb 33348 wl-lem-moexsb 33350 wl-mo2tf 33353 wl-eutf 33355 wl-mo2t 33357 wl-mo3t 33358 wl-sb8eut 33359 wl-ax11-lem2 33363 nfbii2 33967 prtlem14 34159 axc5 34178 setindtr 37591 pm11.57 38589 pm11.59 38591 axc5c4c711toc7 38605 axc5c4c711to11 38606 axc11next 38607 iotain 38618 eubi 38637 ssralv2 38737 19.41rg 38766 hbexg 38772 ax6e2ndeq 38775 ssralv2VD 39102 19.41rgVD 39138 hbimpgVD 39140 hbexgVD 39142 ax6e2eqVD 39143 ax6e2ndeqVD 39145 vk15.4jVD 39150 ax6e2ndeqALT 39167 rexsb 41168 setrec1lem4 42437 |
Copyright terms: Public domain | W3C validator |