NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  sp GIF version

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.
StepHypRef Expression
1 a9ev 1656 . 2 w w = x
2 equcomi 1679 . . . . . 6 (w = xx = w)
3 ax-17 1616 . . . . . 6 φw ¬ φ)
4 ax-11 1746 . . . . . 6 (x = w → (w ¬ φx(x = w → ¬ φ)))
52, 3, 4syl2im 34 . . . . 5 (w = x → (¬ φx(x = w → ¬ φ)))
6 ax9v 1655 . . . . . 6 ¬ x ¬ x = w
7 con2 108 . . . . . . 7 ((x = w → ¬ φ) → (φ → ¬ x = w))
87al2imi 1561 . . . . . 6 (x(x = w → ¬ φ) → (xφx ¬ x = w))
96, 8mtoi 169 . . . . 5 (x(x = w → ¬ φ) → ¬ xφ)
105, 9syl6 29 . . . 4 (w = x → (¬ φ → ¬ xφ))
1110con4d 97 . . 3 (w = x → (xφφ))
1211exlimiv 1634 . 2 (w w = x → (xφφ))
131, 12ax-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