Theorem sp 2188

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

This theorem shows that our obsolete axiom ax-c5 39055 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 2182. 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 2186	. . 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 2182

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

This theorem is referenced by:  spi  2189  sps  2190  2sp  2191  spsd  2192  19.21bi  2194  19.3t  2206  19.3  2207  19.9d  2208  sb4av  2249  sbequ2  2254  axc16gb  2267  axc7  2320  axc4  2324  19.12  2330  exsb  2361  ax12  2425  ax12b  2426  ax13ALT  2427  hbae  2433  sb4a  2482  dfsb2  2495  nfsb4t  2501  mo3  2561  mopick  2622  axi4  2696  axi5r  2697  nfcrALT  2886  rsp  3221  ceqex  3603  elrab3t  3642  abidnf  3657  mob2  3670  sbcnestgfw  4370  sbcnestgf  4375  ralidm  4467  mpteq12f  5180  axrep2  5224  axnulALT  5246  eusv1  5333  alxfr  5349  axprlem4OLD  5371  axprlem5OLD  5372  iota1  6468  dffv2  6926  fiint  9222  isf32lem9  10263  nd3  10491  axrepnd  10496  axpowndlem2  10500  axpowndlem3  10501  axacndlem4  10512  trclfvcotr  14923  relexpindlem  14977  fiinopn  22836  ex-natded9.26-2  30421  bnj1294  34901  bnj570  34989  bnj953  35023  bnj1204  35096  bnj1388  35117  in-ax8  36340  ss-ax8  36341  bj-ssbid2ALT  36780  bj-sb  36804  bj-spst  36806  bj-19.21bit  36807  bj-substax12  36838  bj-hbaeb2  36935  bj-hbnaeb  36937  bj-sbsb  36954  bj-nfcsym  37016  exlimim  37459  exellim  37461  difunieq  37491  wl-aleq  37652  wl-equsal1i  37661  wl-sb8t  37669  wl-2spsbbi  37682  wl-lem-exsb  37683  wl-lem-moexsb  37685  wl-mo2tf  37688  wl-eutf  37690  wl-mo2t  37692  wl-mo3t  37693  wl-sb8eut  37695  mopickr  38468  prtlem14  39046  axc5  39065  setindtr  43181  unielss  43375  ismnushort  44458  pm11.57  44546  pm11.59  44548  axc5c4c711toc7  44561  axc5c4c711to11  44562  axc11next  44563  ssralv2  44688  19.41rg  44707  hbexg  44713  ax6e2ndeq  44716  ssralv2VD  45022  19.41rgVD  45058  hbimpgVD  45060  hbexgVD  45062  ax6e2eqVD  45063  ax6e2ndeqVD  45065  vk15.4jVD  45070  ax6e2ndeqALT  45087  rexsb  47261  ichnfimlem  47625  setrec1lem4  49851