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 2341. This theorem shows that our obsolete axiom ax-c5 33186 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 2034. It is thought the best we can do using only Tarski's axioms is spw 1954. (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 1743 | . 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑) | |
2 | 19.8a 2039 | . . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑) | |
3 | 2 | con1i 143 | . 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑) |
4 | 1, 3 | sylbi 206 | 1 ⊢ (∀𝑥𝜑 → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1473 ∃wex 1695 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-12 2034 |
This theorem depends on definitions: df-bi 196 df-ex 1696 |
This theorem is referenced by: spi 2042 sps 2043 2sp 2044 spsd 2045 19.21bi 2047 19.3 2057 19.9d 2058 axc4 2115 axc7 2117 axc7e 2118 axc16gb 2121 sb56 2136 19.12 2150 nfaldOLD 2152 nfrOLD 2176 19.3OLD 2190 ax12 2292 ax13OLD 2293 hbae 2303 ax12OLD 2329 ax12b 2333 sb2 2340 dfsb2 2361 sbequi 2363 nfsb4t 2377 exsb 2456 mo3 2495 mopick 2523 axi4 2581 axi5r 2582 nfcr 2743 rsp 2913 ceqex 3303 elrab3t 3330 abidnf 3342 mob2 3353 sbcnestgf 3947 mpteq12f 4661 axrep2 4701 axnulALT 4715 dtru 4783 eusv1 4786 alxfr 4804 iota1 5782 dffv2 6181 fiint 8122 isf32lem9 9066 nd3 9290 axrepnd 9295 axpowndlem2 9299 axpowndlem3 9300 axacndlem4 9311 trclfvcotr 13598 relexpindlem 13651 fiinopn 20531 ex-natded9.26-2 26669 bnj1294 30142 bnj570 30229 bnj953 30263 bnj1204 30334 bnj1388 30355 frmin 30983 bj-hbxfrbi 31792 bj-ssbft 31831 bj-ssbequ2 31832 bj-ssbid2ALT 31835 bj-sb 31864 bj-spst 31866 bj-19.21bit 31867 bj-19.3t 31876 bj-sb2v 31941 bj-axrep2 31977 bj-dtru 31985 bj-hbaeb2 31993 bj-hbnaeb 31995 bj-sbsb 32012 bj-nfcsym 32079 bj-ax9 32083 exlimim 32365 exellim 32368 wl-aleq 32501 wl-equsal1i 32508 wl-sb8t 32512 wl-lem-exsb 32527 wl-lem-moexsb 32529 wl-mo2tf 32532 wl-eutf 32534 wl-mo2t 32536 wl-mo3t 32537 wl-sb8eut 32538 wl-ax11-lem2 32542 nfbii2 33137 prtlem14 33177 axc5 33196 setindtr 36609 pm11.57 37611 pm11.59 37613 axc5c4c711toc7 37627 axc5c4c711to11 37628 axc11next 37629 iotain 37640 eubi 37659 ssralv2 37758 19.41rg 37787 hbexg 37793 ax6e2ndeq 37796 ssralv2VD 38124 19.41rgVD 38160 hbimpgVD 38162 hbexgVD 38164 ax6e2eqVD 38165 ax6e2ndeqVD 38167 vk15.4jVD 38172 ax6e2ndeqALT 38189 rexsb 39817 setrec1lem4 42236 |
Copyright terms: Public domain | W3C validator |