Theorem sp 2219

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

This theorem shows that our obsolete axiom ax-c5 40034 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 2212. It is thought the best we can do using only Tarski's axioms is spw 2066. Also see spvw 2013 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 1858	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		19.8a 2217	. . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
3	2	con1i 148	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑)
4	1, 3	sylbi 220	1 ⊢ (∀𝑥𝜑 → 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1567  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-ex 1812

This theorem is used by:  spi  2220  sps  2221  2sp  2222  spsd  2223  19.21bi  2225  19.3t  2237  19.3  2238  19.9d  2239  sb4av  2279  sbequ2  2284  axc16gb  2296  axc7  2347  axc4  2351  19.12  2357  exsb  2388  ax12  2452  ax12b  2453  ax13ALT  2454  hbae  2460  sb4a  2509  dfsb2  2522  nfsb4t  2528  mo3  2589  mopick  2650  axi4  2723  axi5r  2724  nfcrALT  2913  rsp  3250  ceqex  3605  elrab3t  3643  abidnf  3659  mob2  3672  sbcnestgfw  4378  sbcnestgf  4383  ralidm  4472  mpteq12f  5189  axrep2  5234  axnulALT  5257  eusv1  5352  alxfr  5368  iota1  6517  dffv2  6981  fiint  9322  setrec1lem4  9975  isf32lem9  10443  nd3  10678  axrepnd  10683  axpowndlem2  10687  axpowndlem3  10688  axacndlem4  10699  trclfvcotr  15168  relexpindlem  15222  fiinopn  23225  ex-natded9.26-2  31027  bnj1294  35494  bnj570  35582  bnj953  35616  bnj1204  35689  bnj1388  35710  axsepg4  35868  in-ax8  37106  ss-ax8  37107  mh-setindnd  37418  bj-ssbid2ALT  37655  bj-sb  37682  bj-spst  37684  bj-19.21bit  37685  bj-hbext  37706  bj-substax12  37719  bj-hbaeb2  37823  bj-hbnaeb  37825  bj-sbsb  37842  bj-nfcsym  37904  exlimim  38359  exellim  38361  difunieq  38391  wl-aleq  38561  wl-equsal1i  38570  wl-sb8t  38578  wl-2spsbbi  38591  wl-lem-exsb  38592  wl-lem-moexsb  38594  wl-mo2tf  38597  wl-eutf  38599  wl-mo2t  38601  wl-mo3t  38602  wl-sb8eut  38604  findcard4  38726  mopickr  39397  prtlem14  40025  axc5  40044  setindtr  44125  unielss  44314  ismnushort  45379  pm11.57  45467  pm11.59  45469  axc5c4c711toc7  45482  axc5c4c711to11  45483  axc11next  45484  ssralv2  45608  19.41rg  45627  hbexg  45633  ax6e2ndeq  45636  ssralv2VD  45942  19.41rgVD  45978  hbimpgVD  45980  hbexgVD  45982  ax6e2eqVD  45983  ax6e2ndeqVD  45985  vk15.4jVD  45990  ax6e2ndeqALT  46007  quantgodel  47978  rexsb  48263  ichnfimlem  48639