![]() |
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 2428. This theorem shows that our obsolete axiom ax-c5 35039 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 2163. It is thought the best we can do using only Tarski's axioms is spw 2084. (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 1869 | . 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑) | |
2 | 19.8a 2166 | . . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑) | |
3 | 2 | con1i 147 | . 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑) |
4 | 1, 3 | sylbi 209 | 1 ⊢ (∀𝑥𝜑 → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1599 ∃wex 1823 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-12 2163 |
This theorem depends on definitions: df-bi 199 df-ex 1824 |
This theorem is referenced by: spi 2168 sps 2169 2sp 2170 spsd 2171 19.21bi 2173 19.3t 2185 19.3 2186 19.9d 2187 19.9dOLDOLD 2188 axc16gb 2235 sb2v 2243 sb56 2248 spsbimv 2283 axc7 2292 axc4 2296 axc7eOLD 2298 19.12 2303 exsb 2327 ax12 2389 ax12b 2390 ax13ALT 2391 hbae 2397 sb2 2427 dfsb2 2449 sbequi 2451 nfsb4t 2465 exsbOLD 2548 mo3 2580 mo3OLD 2581 mopick 2662 axi4 2743 axi5r 2744 nfcr 2924 rsp 3111 ceqex 3536 elrab3t 3571 abidnf 3585 mob2 3598 sbcbi2 3705 sbcnestgf 4220 mpteq12f 4967 axrep2 5009 axnulALT 5023 dtru 5082 eusv1 5103 alxfr 5119 iota1 6113 dffv2 6531 fiint 8525 isf32lem9 9518 nd3 9746 axrepnd 9751 axpowndlem2 9755 axpowndlem3 9756 axacndlem4 9767 trclfvcotr 14157 relexpindlem 14210 fiinopn 21113 ex-natded9.26-2 27852 bnj1294 31487 bnj570 31574 bnj953 31608 bnj1204 31679 bnj1388 31700 frmin 32331 bj-hbxfrbi 33187 bj-ssbft 33232 bj-ssbequ2 33233 bj-ssbid2ALT 33236 bj-sb 33266 bj-spst 33268 bj-19.21bit 33269 bj-axrep2 33366 bj-dtru 33373 bj-hbaeb2 33380 bj-hbnaeb 33382 bj-sbsb 33399 bj-nfcsym 33457 exlimim 33785 exellim 33787 wl-aleq 33916 wl-equsal1i 33923 wl-sb8t 33928 wl-lem-exsb 33942 wl-lem-moexsb 33944 wl-mo2tf 33947 wl-eutf 33949 wl-mo2t 33951 wl-mo3t 33952 wl-sb8eut 33953 wl-ax11-lem2 33957 nfbii2OLD 34591 prtlem14 35030 axc5 35049 setindtr 38554 pm11.57 39549 pm11.59 39551 axc5c4c711toc7 39564 axc5c4c711to11 39565 axc11next 39566 iotain 39577 eubiOLD 39596 ssralv2 39695 19.41rg 39714 hbexg 39720 ax6e2ndeq 39723 ssralv2VD 40039 19.41rgVD 40075 hbimpgVD 40077 hbexgVD 40079 ax6e2eqVD 40080 ax6e2ndeqVD 40082 vk15.4jVD 40087 ax6e2ndeqALT 40104 rexsb 42131 setrec1lem4 43546 |
Copyright terms: Public domain | W3C validator |