Theorem sp 2195

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

This theorem shows that our obsolete axiom ax-c5 39375 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 2189. It is thought the best we can do using only Tarski's axioms is spw 2041. Also see spvw 1988 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 1833	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		19.8a 2193	. . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
3	2	con1i 147	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑)
4	1, 3	sylbi 218	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1545  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  spi  2196  sps  2197  2sp  2198  spsd  2199  19.21bi  2201  19.3t  2213  19.3  2214  19.9d  2215  sb4av  2256  sbequ2  2261  axc16gb  2274  axc7  2326  axc4  2330  19.12  2336  exsb  2367  ax12  2431  ax12b  2432  ax13ALT  2433  hbae  2439  sb4a  2488  dfsb2  2501  nfsb4t  2507  mo3  2568  mopick  2629  axi4  2702  axi5r  2703  nfcrALT  2892  rsp  3227  ceqex  3590  elrab3t  3628  abidnf  3643  mob2  3656  sbcnestgfw  4349  sbcnestgf  4354  ralidm  4445  mpteq12f  5157  axrep2  5202  axnulALT  5226  eusv1  5320  alxfr  5336  axprlem4OLD  5359  axprlem5OLD  5360  iota1  6464  dffv2  6922  fiint  9227  isf32lem9  10274  nd3  10503  axrepnd  10508  axpowndlem2  10512  axpowndlem3  10513  axacndlem4  10524  trclfvcotr  14962  relexpindlem  15016  fiinopn  22884  ex-natded9.26-2  30508  bnj1294  34999  bnj570  35087  bnj953  35121  bnj1204  35194  bnj1388  35215  axsepg4  35324  in-ax8  36452  ss-ax8  36453  mh-setindnd  36765  bj-ssbid2ALT  37003  bj-sb  37030  bj-spst  37032  bj-19.21bit  37033  bj-hbext  37054  bj-substax12  37067  bj-hbaeb2  37171  bj-hbnaeb  37173  bj-sbsb  37190  bj-nfcsym  37252  exlimim  37704  exellim  37706  difunieq  37736  wl-aleq  37906  wl-equsal1i  37915  wl-sb8t  37923  wl-2spsbbi  37936  wl-lem-exsb  37937  wl-lem-moexsb  37939  wl-mo2tf  37942  wl-eutf  37944  wl-mo2t  37946  wl-mo3t  37947  wl-sb8eut  37949  mopickr  38738  prtlem14  39366  axc5  39385  setindtr  43469  unielss  43663  ismnushort  44745  pm11.57  44833  pm11.59  44835  axc5c4c711toc7  44848  axc5c4c711to11  44849  axc11next  44850  ssralv2  44975  19.41rg  44994  hbexg  45000  ax6e2ndeq  45003  ssralv2VD  45309  19.41rgVD  45345  hbimpgVD  45347  hbexgVD  45349  ax6e2eqVD  45350  ax6e2ndeqVD  45352  vk15.4jVD  45357  ax6e2ndeqALT  45374  quantgodel  47317  rexsb  47562  ichnfimlem  47938  setrec1lem4  50180