Theorem sp 2217

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

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1557  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-ex 1799

This theorem is referenced by:  spi  2218  sps  2219  2sp  2220  spsd  2221  19.21bi  2223  19.3t  2235  19.3  2236  19.9d  2237  sb4av  2278  sbequ2  2283  axc16gb  2296  axc7  2348  axc4  2352  19.12  2358  exsb  2389  ax12  2453  ax12b  2454  ax13ALT  2455  hbae  2461  sb4a  2510  dfsb2  2523  nfsb4t  2529  mo3  2590  mopick  2651  axi4  2724  axi5r  2725  nfcrALT  2914  rsp  3249  ceqex  3610  elrab3t  3648  abidnf  3663  mob2  3676  sbcnestgfw  4372  sbcnestgf  4377  ralidm  4468  mpteq12f  5182  axrep2  5227  axnulALT  5251  eusv1  5345  alxfr  5361  axprlem4OLD  5384  axprlem5OLD  5385  iota1  6495  dffv2  6957  fiint  9265  isf32lem9  10312  nd3  10541  axrepnd  10546  axpowndlem2  10550  axpowndlem3  10551  axacndlem4  10562  trclfvcotr  15016  relexpindlem  15070  fiinopn  22949  ex-natded9.26-2  30579  bnj1294  35073  bnj570  35161  bnj953  35195  bnj1204  35268  bnj1388  35289  axsepg4  35400  in-ax8  36545  ss-ax8  36546  mh-setindnd  36858  bj-ssbid2ALT  37096  bj-sb  37123  bj-spst  37125  bj-19.21bit  37126  bj-hbext  37147  bj-substax12  37160  bj-hbaeb2  37264  bj-hbnaeb  37266  bj-sbsb  37283  bj-nfcsym  37345  exlimim  37797  exellim  37799  difunieq  37829  wl-aleq  37999  wl-equsal1i  38008  wl-sb8t  38016  wl-2spsbbi  38029  wl-lem-exsb  38030  wl-lem-moexsb  38032  wl-mo2tf  38035  wl-eutf  38037  wl-mo2t  38039  wl-mo3t  38040  wl-sb8eut  38042  mopickr  38831  prtlem14  39459  axc5  39478  setindtr  43562  unielss  43756  ismnushort  44838  pm11.57  44926  pm11.59  44928  axc5c4c711toc7  44941  axc5c4c711to11  44942  axc11next  44943  ssralv2  45068  19.41rg  45087  hbexg  45093  ax6e2ndeq  45096  ssralv2VD  45402  19.41rgVD  45438  hbimpgVD  45440  hbexgVD  45442  ax6e2eqVD  45443  ax6e2ndeqVD  45445  vk15.4jVD  45450  ax6e2ndeqALT  45467  quantgodel  47409  rexsb  47654  ichnfimlem  48030  setrec1lem4  50272