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 2064. This theorem shows that our obsolete axiom ax-c5 35899 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 2167. It is thought the best we can do using only Tarski's axioms is spw 2032. Also see spvw 1976 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 1817 | . 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑) | |
2 | 19.8a 2170 | . . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑) | |
3 | 2 | con1i 149 | . 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑) |
4 | 1, 3 | sylbi 218 | 1 ⊢ (∀𝑥𝜑 → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1526 ∃wex 1771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-12 2167 |
This theorem depends on definitions: df-bi 208 df-ex 1772 |
This theorem is referenced by: spi 2173 sps 2174 2sp 2175 spsd 2176 19.21bi 2178 19.3t 2191 19.3 2192 19.9d 2193 sb4av 2234 sbequ2 2240 sbequ2OLD 2241 axc16gb 2253 sb56OLD 2269 spsbimvOLD 2319 axc7 2327 axc4 2331 19.12 2337 exsb 2369 ax12 2437 ax12b 2438 ax13ALT 2439 hbae 2445 sb4a 2502 sb2vOLDOLD 2505 dfsb2 2525 sbequiOLD 2527 nfsb4t 2532 sb2vOLDALT 2576 sb2ALT 2580 dfsb2ALT 2584 sbequiALT 2589 nfsb4tALT 2597 mo3 2641 mopick 2703 axi4 2779 axi5r 2780 nfcr 2963 nfabdw 2997 rsp 3202 ralcom2w 3360 ceqex 3642 elrab3t 3676 abidnf 3691 mob2 3703 sbcbi2 3828 sbcnestgfw 4367 sbcnestgf 4372 mpteq12f 5140 axrep2 5184 axnulALT 5199 dtru 5262 eusv1 5282 alxfr 5298 axprlem4 5317 axprlem5 5318 iota1 6325 dffv2 6749 fiint 8783 isf32lem9 9771 nd3 9999 axrepnd 10004 axpowndlem2 10008 axpowndlem3 10009 axacndlem4 10020 trclfvcotr 14357 relexpindlem 14410 fiinopn 21437 ex-natded9.26-2 28126 bnj1294 31988 bnj570 32076 bnj953 32110 bnj1204 32181 bnj1388 32202 frmin 32981 bj-ssbid2ALT 33893 bj-sb 33918 bj-spst 33920 bj-19.21bit 33921 bj-dtru 34036 bj-hbaeb2 34038 bj-hbnaeb 34040 bj-sbsb 34057 bj-nfcsym 34112 exlimim 34505 exellim 34507 difunieq 34537 wl-aleq 34656 wl-equsal1i 34664 wl-sb8t 34669 wl-2spsbbi 34682 wl-lem-exsb 34683 wl-lem-moexsb 34685 wl-mo2tf 34688 wl-eutf 34690 wl-mo2t 34692 wl-mo3t 34693 wl-sb8eut 34694 wl-ax11-lem2 34699 prtlem14 35890 axc5 35909 setindtr 39499 pm11.57 40598 pm11.59 40600 axc5c4c711toc7 40613 axc5c4c711to11 40614 axc11next 40615 eubiOLD 40645 ssralv2 40742 19.41rg 40761 hbexg 40767 ax6e2ndeq 40770 ssralv2VD 41077 19.41rgVD 41113 hbimpgVD 41115 hbexgVD 41117 ax6e2eqVD 41118 ax6e2ndeqVD 41120 vk15.4jVD 41125 ax6e2ndeqALT 41142 rexsb 43174 setrec1lem4 44721 |
Copyright terms: Public domain | W3C validator |