Theorem sp 1747

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.)

Assertion

Ref	Expression
sp	⊢ (∀xφ → φ)

Proof of Theorem sp

Dummy variable w is distinct from all other variables.

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φ → φ)

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  2482  rsp  2675  ceqex  2970  abidnf  3006  mob2  3017  csbie2t  3181  sbcnestgf  3184  iota1  4354  copsex2t  4609  ssopab2  4713  funun  5147  fununi  5161  mpteq12f  5656  fnfullfunlem2  5858  fundmen  6044