| 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 39143 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 2184. 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 2188 | . . 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 2184 |
| This theorem depends on definitions: df-bi 207 df-ex 1781 |
| This theorem is referenced by: spi 2191 sps 2192 2sp 2193 spsd 2194 19.21bi 2196 19.3t 2208 19.3 2209 19.9d 2210 sb4av 2251 sbequ2 2256 axc16gb 2269 axc7 2322 axc4 2326 19.12 2332 exsb 2363 ax12 2427 ax12b 2428 ax13ALT 2429 hbae 2435 sb4a 2484 dfsb2 2497 nfsb4t 2503 mo3 2564 mopick 2625 axi4 2699 axi5r 2700 nfcrALT 2889 rsp 3224 ceqex 3606 elrab3t 3645 abidnf 3660 mob2 3673 sbcnestgfw 4373 sbcnestgf 4378 ralidm 4470 mpteq12f 5183 axrep2 5227 axnulALT 5249 eusv1 5336 alxfr 5352 axprlem4OLD 5374 axprlem5OLD 5375 iota1 6471 dffv2 6929 fiint 9227 isf32lem9 10271 nd3 10500 axrepnd 10505 axpowndlem2 10509 axpowndlem3 10510 axacndlem4 10521 trclfvcotr 14932 relexpindlem 14986 fiinopn 22845 ex-natded9.26-2 30495 bnj1294 34973 bnj570 35061 bnj953 35095 bnj1204 35168 bnj1388 35189 in-ax8 36418 ss-ax8 36419 mh-setindnd 36667 bj-ssbid2ALT 36864 bj-sb 36888 bj-spst 36890 bj-19.21bit 36891 bj-substax12 36922 bj-hbaeb2 37019 bj-hbnaeb 37021 bj-sbsb 37038 bj-nfcsym 37100 exlimim 37547 exellim 37549 difunieq 37579 wl-aleq 37740 wl-equsal1i 37749 wl-sb8t 37757 wl-2spsbbi 37770 wl-lem-exsb 37771 wl-lem-moexsb 37773 wl-mo2tf 37776 wl-eutf 37778 wl-mo2t 37780 wl-mo3t 37781 wl-sb8eut 37783 mopickr 38556 prtlem14 39134 axc5 39153 setindtr 43266 unielss 43460 ismnushort 44542 pm11.57 44630 pm11.59 44632 axc5c4c711toc7 44645 axc5c4c711to11 44646 axc11next 44647 ssralv2 44772 19.41rg 44791 hbexg 44797 ax6e2ndeq 44800 ssralv2VD 45106 19.41rgVD 45142 hbimpgVD 45144 hbexgVD 45146 ax6e2eqVD 45147 ax6e2ndeqVD 45149 vk15.4jVD 45154 ax6e2ndeqALT 45171 rexsb 47345 ichnfimlem 47709 setrec1lem4 49935 |
| Copyright terms: Public domain | W3C validator |