New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > sp | 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).
For the axiom of specialization presented in many logic textbooks, see Theorem stdpc4 2024. This theorem shows that our obsolete axiom ax-4 2135 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-11 1746. It is thought the best we can do using only Tarski's axioms is spw 1694. (Contributed by NM, 21-May-2008.) (Proof shortened by Scott Fenton, 24-Jan-2011.) (Proof shortened by Wolf Lammen, 23-Dec-2017.) |
Ref | Expression |
---|---|
sp | ⊢ (∀xφ → φ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | a9ev 1656 | . 2 ⊢ ∃w w = x | |
2 | equcomi 1679 | . . . . . 6 ⊢ (w = x → x = w) | |
3 | ax-17 1616 | . . . . . 6 ⊢ (¬ φ → ∀w ¬ φ) | |
4 | ax-11 1746 | . . . . . 6 ⊢ (x = w → (∀w ¬ φ → ∀x(x = w → ¬ φ))) | |
5 | 2, 3, 4 | syl2im 34 | . . . . 5 ⊢ (w = x → (¬ φ → ∀x(x = w → ¬ φ))) |
6 | ax9v 1655 | . . . . . 6 ⊢ ¬ ∀x ¬ x = w | |
7 | con2 108 | . . . . . . 7 ⊢ ((x = w → ¬ φ) → (φ → ¬ x = w)) | |
8 | 7 | al2imi 1561 | . . . . . 6 ⊢ (∀x(x = w → ¬ φ) → (∀xφ → ∀x ¬ x = w)) |
9 | 6, 8 | mtoi 169 | . . . . 5 ⊢ (∀x(x = w → ¬ φ) → ¬ ∀xφ) |
10 | 5, 9 | syl6 29 | . . . 4 ⊢ (w = x → (¬ φ → ¬ ∀xφ)) |
11 | 10 | con4d 97 | . . 3 ⊢ (w = x → (∀xφ → φ)) |
12 | 11 | exlimiv 1634 | . 2 ⊢ (∃w w = x → (∀xφ → φ)) |
13 | 1, 12 | ax-mp 5 | 1 ⊢ (∀xφ → φ) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1540 ∃wex 1541 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-11 1746 |
This theorem depends on definitions: df-bi 177 df-ex 1542 |
This theorem is referenced by: ax5o 1749 ax6o 1750 spi 1753 sps 1754 spsd 1755 19.8a 1756 19.21bi 1758 nfr 1761 hbnOLD 1777 19.3 1785 hba1OLD 1787 hbimdOLD 1816 spimehOLD 1821 equsalhwOLD 1839 19.21hOLD 1840 19.12 1847 19.12OLD 1848 cbv3hvOLD 1851 nfald 1852 19.21tOLD 1863 19.38OLD 1874 ax12olem3 1929 ax12 1935 dvelimv 1939 ax9 1949 hbae 1953 spimt 1974 equveli 1988 ax11b 1995 sb2 2023 a16gb 2050 dfsb2 2055 nfsb4t 2080 sb56 2098 sb6 2099 sbal1 2126 exsb 2130 ax4 2145 mo 2226 mopick 2266 2eu1 2284 axi4 2325 axi5r 2326 nfcr 2481 rsp 2674 ceqex 2969 abidnf 3005 mob2 3016 csbie2t 3180 sbcnestgf 3183 iota1 4353 copsex2t 4608 ssopab2 4712 funun 5146 fununi 5160 mpteq12f 5655 fnfullfunlem2 5857 fundmen 6043 |
Copyright terms: Public domain | W3C validator |