| 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 2068. This theorem shows that our obsolete axiom ax-c5 38884 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 2177. It is thought the best we can do using only Tarski's axioms is spw 2033. Also see spvw 1980 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 1826 | . 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑) | |
| 2 | 19.8a 2181 | . . 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 1538 ∃wex 1779 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 |
| This theorem is referenced by: spi 2184 sps 2185 2sp 2186 spsd 2187 19.21bi 2189 19.3t 2201 19.3 2202 19.9d 2203 sb4av 2244 sbequ2 2249 axc16gb 2262 axc7 2317 axc4 2321 19.12 2327 exsb 2362 ax12 2428 ax12b 2429 ax13ALT 2430 hbae 2436 sb4a 2485 dfsb2 2498 nfsb4t 2504 mo3 2564 mopick 2625 axi4 2699 axi5r 2700 nfcrALT 2896 rsp 3247 ceqex 3652 elrab3t 3691 abidnf 3708 mob2 3721 sbcnestgfw 4421 sbcnestgf 4426 ralidm 4512 mpteq12f 5230 axrep2 5282 axnulALT 5304 eusv1 5391 alxfr 5407 axprlem4OLD 5429 axprlem5OLD 5430 iota1 6538 dffv2 7004 fiint 9366 fiintOLD 9367 isf32lem9 10401 nd3 10629 axrepnd 10634 axpowndlem2 10638 axpowndlem3 10639 axacndlem4 10650 trclfvcotr 15048 relexpindlem 15102 fiinopn 22907 ex-natded9.26-2 30439 bnj1294 34831 bnj570 34919 bnj953 34953 bnj1204 35026 bnj1388 35047 in-ax8 36225 ss-ax8 36226 bj-ssbid2ALT 36664 bj-sb 36688 bj-spst 36690 bj-19.21bit 36691 bj-substax12 36722 bj-hbaeb2 36819 bj-hbnaeb 36821 bj-sbsb 36838 bj-nfcsym 36900 exlimim 37343 exellim 37345 difunieq 37375 wl-aleq 37536 wl-equsal1i 37545 wl-sb8t 37553 wl-2spsbbi 37566 wl-lem-exsb 37567 wl-lem-moexsb 37569 wl-mo2tf 37572 wl-eutf 37574 wl-mo2t 37576 wl-mo3t 37577 wl-sb8eut 37579 wl-ax11-lem2 37587 mopickr 38364 prtlem14 38875 axc5 38894 setindtr 43036 unielss 43230 ismnushort 44320 pm11.57 44408 pm11.59 44410 axc5c4c711toc7 44423 axc5c4c711to11 44424 axc11next 44425 eubiOLD 44455 ssralv2 44551 19.41rg 44570 hbexg 44576 ax6e2ndeq 44579 ssralv2VD 44886 19.41rgVD 44922 hbimpgVD 44924 hbexgVD 44926 ax6e2eqVD 44927 ax6e2ndeqVD 44929 vk15.4jVD 44934 ax6e2ndeqALT 44951 rexsb 47111 ichnfimlem 47450 setrec1lem4 49209 |
| Copyright terms: Public domain | W3C validator |