Theorem sp 2180

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 36179 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 2175. It is thought the best we can do using only Tarski's axioms is spw 2041. Also see spvw 1985 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 2178	. . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
3	2	con1i 149	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑)
4	1, 3	sylbi 220	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1536  ∃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 1911  ax-6 1970  ax-7 2015  ax-12 2175

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

This theorem is referenced by:  spi  2181  sps  2182  2sp  2183  spsd  2184  19.21bi  2186  19.3t  2199  19.3  2200  19.9d  2201  sb4av  2242  sbequ2  2247  sbequ2OLD  2248  axc16gb  2260  sb56OLD  2275  axc7  2325  axc4  2329  19.12  2335  exsb  2367  ax12  2434  ax12b  2435  ax13ALT  2436  hbae  2442  sb4a  2498  dfsb2  2511  nfsb4t  2517  sb2vOLDALT  2559  sb2ALT  2563  dfsb2ALT  2567  sbequiALT  2572  nfsb4tALT  2580  mo3  2623  mopick  2687  axi4  2761  axi5r  2762  nfcrALT  2942  nfcriOLDOLD  2947  nfabdw  2976  rsp  3170  ceqex  3593  elrab3t  3627  abidnf  3642  mob2  3654  sbcbi2OLD  3779  sbcnestgfw  4326  sbcnestgf  4331  mpteq12f  5113  axrep2  5157  axnulALT  5172  dtru  5236  eusv1  5257  alxfr  5273  axprlem4  5292  axprlem5  5293  iota1  6301  dffv2  6733  fiint  8779  isf32lem9  9772  nd3  10000  axrepnd  10005  axpowndlem2  10009  axpowndlem3  10010  axacndlem4  10021  trclfvcotr  14360  relexpindlem  14414  fiinopn  21506  ex-natded9.26-2  28205  bnj1294  32199  bnj570  32287  bnj953  32321  bnj1204  32394  bnj1388  32415  frmin  33197  bj-ssbid2ALT  34109  bj-sb  34134  bj-spst  34136  bj-19.21bit  34137  bj-subst  34168  bj-dtru  34254  bj-hbaeb2  34256  bj-hbnaeb  34258  bj-sbsb  34275  bj-nfcsym  34339  exlimim  34759  exellim  34761  difunieq  34791  wl-aleq  34940  wl-equsal1i  34948  wl-sb8t  34953  wl-2spsbbi  34966  wl-lem-exsb  34967  wl-lem-moexsb  34969  wl-mo2tf  34972  wl-eutf  34974  wl-mo2t  34976  wl-mo3t  34977  wl-sb8eut  34978  wl-ax11-lem2  34983  prtlem14  36170  axc5  36189  setindtr  39965  pm11.57  41093  pm11.59  41095  axc5c4c711toc7  41108  axc5c4c711to11  41109  axc11next  41110  eubiOLD  41140  ssralv2  41237  19.41rg  41256  hbexg  41262  ax6e2ndeq  41265  ssralv2VD  41572  19.41rgVD  41608  hbimpgVD  41610  hbexgVD  41612  ax6e2eqVD  41613  ax6e2ndeqVD  41615  vk15.4jVD  41620  ax6e2ndeqALT  41637  rexsb  43654  ichnfimlem  43980  setrec1lem4  45220