Theorem sp 2186

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

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1539  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2180

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

This theorem is referenced by:  spi  2187  sps  2188  2sp  2189  spsd  2190  19.21bi  2192  19.3t  2204  19.3  2205  19.9d  2206  sb4av  2247  sbequ2  2252  axc16gb  2265  axc7  2318  axc4  2322  19.12  2328  exsb  2359  ax12  2423  ax12b  2424  ax13ALT  2425  hbae  2431  sb4a  2480  dfsb2  2493  nfsb4t  2499  mo3  2559  mopick  2620  axi4  2694  axi5r  2695  nfcrALT  2885  rsp  3220  ceqex  3602  elrab3t  3641  abidnf  3656  mob2  3669  sbcnestgfw  4366  sbcnestgf  4371  ralidm  4457  mpteq12f  5171  axrep2  5215  axnulALT  5237  eusv1  5324  alxfr  5340  axprlem4OLD  5362  axprlem5OLD  5363  iota1  6455  dffv2  6912  fiint  9206  isf32lem9  10247  nd3  10475  axrepnd  10480  axpowndlem2  10484  axpowndlem3  10485  axacndlem4  10496  trclfvcotr  14911  relexpindlem  14965  fiinopn  22811  ex-natded9.26-2  30392  bnj1294  34821  bnj570  34909  bnj953  34943  bnj1204  35016  bnj1388  35037  in-ax8  36258  ss-ax8  36259  bj-ssbid2ALT  36697  bj-sb  36721  bj-spst  36723  bj-19.21bit  36724  bj-substax12  36755  bj-hbaeb2  36852  bj-hbnaeb  36854  bj-sbsb  36871  bj-nfcsym  36933  exlimim  37376  exellim  37378  difunieq  37408  wl-aleq  37569  wl-equsal1i  37578  wl-sb8t  37586  wl-2spsbbi  37599  wl-lem-exsb  37600  wl-lem-moexsb  37602  wl-mo2tf  37605  wl-eutf  37607  wl-mo2t  37609  wl-mo3t  37610  wl-sb8eut  37612  wl-ax11-lem2  37620  mopickr  38391  prtlem14  38913  axc5  38932  setindtr  43057  unielss  43251  ismnushort  44334  pm11.57  44422  pm11.59  44424  axc5c4c711toc7  44437  axc5c4c711to11  44438  axc11next  44439  ssralv2  44564  19.41rg  44583  hbexg  44589  ax6e2ndeq  44592  ssralv2VD  44898  19.41rgVD  44934  hbimpgVD  44936  hbexgVD  44938  ax6e2eqVD  44939  ax6e2ndeqVD  44941  vk15.4jVD  44946  ax6e2ndeqALT  44963  rexsb  47130  ichnfimlem  47494  setrec1lem4  49722