![]() |
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 2202. This theorem shows that our obsolete axiom ax-c5 32519 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 1950. It is thought the best we can do using only Tarski's axioms is spw 1884. (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 1706 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 19.8a 1955 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | con1i 134 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | sylbi 200 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-12 1950 |
This theorem depends on definitions: df-bi 190 df-ex 1672 |
This theorem is referenced by: axc4 1958 axc7 1959 spi 1962 sps 1963 2sp 1964 spsd 1965 19.21bi 1967 nfr 1971 19.3 1986 axc16gb 2044 19.12 2052 nfald 2053 sb56 2096 ax13 2155 hbae 2164 ax12 2190 ax12b 2194 sb2 2201 dfsb2 2222 sbequi 2224 nfsb4t 2238 exsb 2317 mo3 2356 mopick 2384 axi4 2442 axi5r 2443 nfcr 2604 rsp 2773 ceqex 3157 abidnf 3195 mob2 3206 sbcnestgf 3788 mpteq12f 4472 axrep2 4510 axnulALT 4524 dtru 4592 eusv1 4595 alxfr 4611 iota1 5567 dffv2 5953 fiint 7866 isf32lem9 8809 nd3 9032 axrepnd 9037 axpowndlem2 9041 axpowndlem3 9042 axacndlem4 9053 trclfvcotr 13150 relexpindlem 13203 fiinopn 20008 ex-natded9.26-2 25949 bnj1294 29701 bnj570 29788 bnj953 29822 bnj1204 29893 bnj1388 29914 frmin 30551 bj-hbxfrbi 31280 bj-ssbft 31319 bj-ssbequ2 31320 bj-ssbid2ALT 31323 bj-spst 31348 bj-19.21bit 31349 bj-19.3t 31358 bj-axc16gb 31423 bj-sb2v 31431 bj-axrep2 31470 bj-dtru 31478 bj-hbaeb2 31486 bj-hbnaeb 31488 bj-sbsb 31505 bj-nfcsym 31562 bj-ax9 31566 exlimim 31814 exellim 31817 wl-aleq 31938 wl-equsal1i 31946 wl-sb8t 31950 wl-lem-exsb 31965 wl-lem-moexsb 31967 wl-mo2tf 31970 wl-eutf 31972 wl-mo2t 31974 wl-mo3t 31975 wl-sb8eut 31976 wl-ax11-lem2 31980 nfbii2 32466 prtlem14 32510 axc5 32529 setindtr 35950 pm11.57 36809 pm11.59 36811 axc5c4c711toc7 36825 axc5c4c711to11 36826 axc11next 36827 iotain 36838 eubi 36857 ssralv2 36958 19.41rg 36987 hbexg 36993 ax6e2ndeq 36996 ssralv2VD 37326 19.41rgVD 37362 hbimpgVD 37364 hbexgVD 37366 ax6e2eqVD 37367 ax6e2ndeqVD 37369 vk15.4jVD 37374 ax6e2ndeqALT 37391 rexsb 38734 |
Copyright terms: Public domain | W3C validator |