![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sp | Structured version Visualization version GIF 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 2381. This theorem shows that our obsolete axiom ax-c5 34487 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 2087. It is thought the best we can do using only Tarski's axioms is spw 2009. (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 1793 | . 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑) | |
2 | 19.8a 2090 | . . 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 1521 ∃wex 1744 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-12 2087 |
This theorem depends on definitions: df-bi 197 df-ex 1745 |
This theorem is referenced by: spi 2092 sps 2093 2sp 2094 spsd 2095 19.21bi 2097 19.3 2107 19.9d 2108 axc4 2168 axc7 2170 axc7e 2171 axc16gb 2174 sb56 2188 19.12 2200 nfaldOLD 2202 nfrOLD 2224 19.3OLD 2238 ax12 2340 ax13ALT 2341 hbae 2348 ax12OLD 2372 ax12b 2373 sb2 2380 dfsb2 2401 sbequi 2403 nfsb4t 2417 exsb 2496 mo3 2536 mopick 2564 axi4 2622 axi5r 2623 nfcr 2785 rsp 2958 ceqex 3364 elrab3t 3395 abidnf 3408 mob2 3419 sbcnestgf 4028 mpteq12f 4764 axrep2 4806 axnulALT 4820 dtru 4887 eusv1 4890 alxfr 4908 iota1 5903 dffv2 6310 fiint 8278 isf32lem9 9221 nd3 9449 axrepnd 9454 axpowndlem2 9458 axpowndlem3 9459 axacndlem4 9470 trclfvcotr 13794 relexpindlem 13847 fiinopn 20754 ex-natded9.26-2 27407 bnj1294 31014 bnj570 31101 bnj953 31135 bnj1204 31206 bnj1388 31227 frmin 31867 bj-hbxfrbi 32733 bj-ssbft 32767 bj-ssbequ2 32768 bj-ssbid2ALT 32771 bj-sb 32802 bj-spst 32804 bj-19.21bit 32805 bj-19.3t 32814 bj-sb2v 32878 bj-axrep2 32914 bj-dtru 32922 bj-hbaeb2 32930 bj-hbnaeb 32932 bj-sbsb 32949 bj-nfcsym 33011 exlimim 33319 exellim 33322 wl-aleq 33452 wl-equsal1i 33459 wl-sb8t 33463 wl-lem-exsb 33478 wl-lem-moexsb 33480 wl-mo2tf 33483 wl-eutf 33485 wl-mo2t 33487 wl-mo3t 33488 wl-sb8eut 33489 wl-ax11-lem2 33493 nfbii2 34097 prtlem14 34478 axc5 34497 setindtr 37908 pm11.57 38906 pm11.59 38908 axc5c4c711toc7 38922 axc5c4c711to11 38923 axc11next 38924 iotain 38935 eubi 38954 ssralv2 39054 19.41rg 39083 hbexg 39089 ax6e2ndeq 39092 ssralv2VD 39416 19.41rgVD 39452 hbimpgVD 39454 hbexgVD 39456 ax6e2eqVD 39457 ax6e2ndeqVD 39459 vk15.4jVD 39464 ax6e2ndeqALT 39481 rexsb 41489 setrec1lem4 42762 |
Copyright terms: Public domain | W3C validator |