| 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 2073. This theorem shows that our obsolete axiom ax-c5 39002 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 2182. It is thought the best we can do using only Tarski's axioms is spw 2035. Also see spvw 1982 where 𝑥 and 𝜑 are disjoint, using fewer axioms. (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 1827 | . 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑) | |
| 2 | 19.8a 2186 | . . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑) | |
| 3 | 2 | con1i 147 | . 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑) |
| 4 | 1, 3 | sylbi 217 | 1 ⊢ (∀𝑥𝜑 → 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∀wal 1539 ∃wex 1780 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-12 2182 |
| This theorem depends on definitions: df-bi 207 df-ex 1781 |
| This theorem is referenced by: spi 2189 sps 2190 2sp 2191 spsd 2192 19.21bi 2194 19.3t 2206 19.3 2207 19.9d 2208 sb4av 2249 sbequ2 2254 axc16gb 2267 axc7 2320 axc4 2324 19.12 2330 exsb 2361 ax12 2425 ax12b 2426 ax13ALT 2427 hbae 2433 sb4a 2482 dfsb2 2495 nfsb4t 2501 mo3 2561 mopick 2622 axi4 2696 axi5r 2697 nfcrALT 2886 rsp 3221 ceqex 3603 elrab3t 3642 abidnf 3657 mob2 3670 sbcnestgfw 4370 sbcnestgf 4375 ralidm 4461 mpteq12f 5178 axrep2 5222 axnulALT 5244 eusv1 5331 alxfr 5347 axprlem4OLD 5369 axprlem5OLD 5370 iota1 6465 dffv2 6923 fiint 9218 isf32lem9 10259 nd3 10487 axrepnd 10492 axpowndlem2 10496 axpowndlem3 10497 axacndlem4 10508 trclfvcotr 14918 relexpindlem 14972 fiinopn 22817 ex-natded9.26-2 30402 bnj1294 34850 bnj570 34938 bnj953 34972 bnj1204 35045 bnj1388 35066 in-ax8 36289 ss-ax8 36290 bj-ssbid2ALT 36728 bj-sb 36752 bj-spst 36754 bj-19.21bit 36755 bj-substax12 36786 bj-hbaeb2 36883 bj-hbnaeb 36885 bj-sbsb 36902 bj-nfcsym 36964 exlimim 37407 exellim 37409 difunieq 37439 wl-aleq 37600 wl-equsal1i 37609 wl-sb8t 37617 wl-2spsbbi 37630 wl-lem-exsb 37631 wl-lem-moexsb 37633 wl-mo2tf 37636 wl-eutf 37638 wl-mo2t 37640 wl-mo3t 37641 wl-sb8eut 37643 mopickr 38415 prtlem14 38993 axc5 39012 setindtr 43141 unielss 43335 ismnushort 44418 pm11.57 44506 pm11.59 44508 axc5c4c711toc7 44521 axc5c4c711to11 44522 axc11next 44523 ssralv2 44648 19.41rg 44667 hbexg 44673 ax6e2ndeq 44676 ssralv2VD 44982 19.41rgVD 45018 hbimpgVD 45020 hbexgVD 45022 ax6e2eqVD 45023 ax6e2ndeqVD 45025 vk15.4jVD 45030 ax6e2ndeqALT 45047 rexsb 47223 ichnfimlem 47587 setrec1lem4 49815 |
| Copyright terms: Public domain | W3C validator |