![]() |
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 2499. This theorem shows that our obsolete axiom ax-c5 34692 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 2203. It is thought the best we can do using only Tarski's axioms is spw 2123. (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 1901 | . 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑) | |
2 | 19.8a 2206 | . . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑) | |
3 | 2 | con1i 146 | . 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑) |
4 | 1, 3 | sylbi 207 | 1 ⊢ (∀𝑥𝜑 → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1629 ∃wex 1852 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-12 2203 |
This theorem depends on definitions: df-bi 197 df-ex 1853 |
This theorem is referenced by: spi 2208 sps 2209 2sp 2210 spsd 2211 19.21bi 2213 19.3 2224 19.9d 2225 19.9dOLDOLD 2226 sb56 2271 sb6 2272 axc4 2294 axc7 2296 axc7eOLD 2298 axc16gb 2301 19.12 2326 nfaldOLD 2328 nfrOLD 2350 19.3OLD 2364 ax12 2460 ax13ALT 2461 hbae 2467 ax12b 2491 sb2 2498 dfsb2 2520 sbequi 2522 nfsb4t 2536 exsb 2616 mo3 2656 mopick 2684 axi4 2742 axi5r 2743 nfcr 2905 rsp 3078 ceqex 3484 elrab3t 3515 abidnf 3528 mob2 3539 sbcnestgf 4140 mpteq12f 4866 axrep2 4908 axnulALT 4922 dtru 4989 eusv1 4992 alxfr 5008 iota1 6009 dffv2 6414 fiint 8394 isf32lem9 9386 nd3 9614 axrepnd 9619 axpowndlem2 9623 axpowndlem3 9624 axacndlem4 9635 trclfvcotr 13959 relexpindlem 14012 fiinopn 20927 ex-natded9.26-2 27620 bnj1294 31227 bnj570 31314 bnj953 31348 bnj1204 31419 bnj1388 31440 frmin 32080 bj-hbxfrbi 32946 bj-ssbft 32980 bj-ssbequ2 32981 bj-ssbid2ALT 32984 bj-sb 33015 bj-spst 33017 bj-19.21bit 33018 bj-19.3t 33027 bj-sb2v 33090 bj-axrep2 33126 bj-dtru 33134 bj-hbaeb2 33141 bj-hbnaeb 33143 bj-sbsb 33160 bj-nfcsym 33216 exlimim 33527 exellim 33530 wl-aleq 33658 wl-equsal1i 33665 wl-sb8t 33669 wl-lem-exsb 33683 wl-lem-moexsb 33685 wl-mo2tf 33688 wl-eutf 33690 wl-mo2t 33692 wl-mo3t 33693 wl-sb8eut 33694 wl-ax11-lem2 33698 nfbii2 34300 prtlem14 34683 axc5 34702 setindtr 38118 pm11.57 39116 pm11.59 39118 axc5c4c711toc7 39132 axc5c4c711to11 39133 axc11next 39134 iotain 39145 eubi 39164 ssralv2 39263 19.41rg 39292 hbexg 39298 ax6e2ndeq 39301 ssralv2VD 39625 19.41rgVD 39661 hbimpgVD 39663 hbexgVD 39665 ax6e2eqVD 39666 ax6e2ndeqVD 39668 vk15.4jVD 39673 ax6e2ndeqALT 39690 rexsb 41689 setrec1lem4 42966 |
Copyright terms: Public domain | W3C validator |