Theorem sp 2191

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

This theorem shows that our obsolete axiom ax-c5 39329 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 2185. It is thought the best we can do using only Tarski's axioms is spw 2036. Also see spvw 1983 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.)

Assertion

Ref	Expression
sp	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem sp

Step	Hyp	Ref	Expression
1		alex 1828	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		19.8a 2189	. . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
3	2	con1i 147	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑)
4	1, 3	sylbi 217	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1540  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  spi  2192  sps  2193  2sp  2194  spsd  2195  19.21bi  2197  19.3t  2209  19.3  2210  19.9d  2211  sb4av  2252  sbequ2  2257  axc16gb  2270  axc7  2322  axc4  2326  19.12  2332  exsb  2363  ax12  2427  ax12b  2428  ax13ALT  2429  hbae  2435  sb4a  2484  dfsb2  2497  nfsb4t  2503  mo3  2564  mopick  2625  axi4  2699  axi5r  2700  nfcrALT  2889  rsp  3225  ceqex  3594  elrab3t  3633  abidnf  3648  mob2  3661  sbcnestgfw  4361  sbcnestgf  4366  ralidm  4457  mpteq12f  5170  axrep2  5215  axnulALT  5239  eusv1  5333  alxfr  5349  axprlem4OLD  5372  axprlem5OLD  5373  iota1  6477  dffv2  6935  fiint  9237  isf32lem9  10283  nd3  10512  axrepnd  10517  axpowndlem2  10521  axpowndlem3  10522  axacndlem4  10533  trclfvcotr  14971  relexpindlem  15025  fiinopn  22866  ex-natded9.26-2  30490  bnj1294  34959  bnj570  35047  bnj953  35081  bnj1204  35154  bnj1388  35175  in-ax8  36406  ss-ax8  36407  mh-setindnd  36719  bj-ssbid2ALT  36957  bj-sb  36984  bj-spst  36986  bj-19.21bit  36987  bj-hbext  37008  bj-substax12  37021  bj-hbaeb2  37125  bj-hbnaeb  37127  bj-sbsb  37144  bj-nfcsym  37206  exlimim  37658  exellim  37660  difunieq  37690  wl-aleq  37860  wl-equsal1i  37869  wl-sb8t  37877  wl-2spsbbi  37890  wl-lem-exsb  37891  wl-lem-moexsb  37893  wl-mo2tf  37896  wl-eutf  37898  wl-mo2t  37900  wl-mo3t  37901  wl-sb8eut  37903  mopickr  38692  prtlem14  39320  axc5  39339  setindtr  43452  unielss  43646  ismnushort  44728  pm11.57  44816  pm11.59  44818  axc5c4c711toc7  44831  axc5c4c711to11  44832  axc11next  44833  ssralv2  44958  19.41rg  44977  hbexg  44983  ax6e2ndeq  44986  ssralv2VD  45292  19.41rgVD  45328  hbimpgVD  45330  hbexgVD  45332  ax6e2eqVD  45333  ax6e2ndeqVD  45335  vk15.4jVD  45340  ax6e2ndeqALT  45357  quantgodel  47302  rexsb  47547  ichnfimlem  47923  setrec1lem4  50165