Theorem sp 2225

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

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1565  ∃wex 1806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

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

This theorem is referenced by:  spi  2226  sps  2227  2sp  2228  spsd  2229  19.21bi  2231  19.3t  2243  19.3  2244  19.9d  2245  sb4av  2286  sbequ2  2291  axc16gb  2304  axc7  2356  axc4  2360  19.12  2366  exsb  2397  ax12  2461  ax12b  2462  ax13ALT  2463  hbae  2469  sb4a  2518  dfsb2  2531  nfsb4t  2537  mo3  2598  mopick  2659  axi4  2732  axi5r  2733  nfcrALT  2922  rsp  3259  ceqex  3620  elrab3t  3658  abidnf  3674  mob2  3687  sbcnestgfw  4384  sbcnestgf  4389  ralidm  4480  mpteq12f  5197  axrep2  5242  axnulALT  5266  eusv1  5360  alxfr  5376  axprlem4OLD  5399  axprlem5OLD  5400  iota1  6512  dffv2  6974  fiint  9282  isf32lem9  10341  nd3  10570  axrepnd  10575  axpowndlem2  10579  axpowndlem3  10580  axacndlem4  10591  trclfvcotr  15042  relexpindlem  15096  fiinopn  23023  ex-natded9.26-2  30708  bnj1294  35146  bnj570  35234  bnj953  35268  bnj1204  35341  bnj1388  35362  axsepg4  35475  in-ax8  36621  ss-ax8  36622  mh-setindnd  36933  bj-ssbid2ALT  37170  bj-sb  37197  bj-spst  37199  bj-19.21bit  37200  bj-hbext  37221  bj-substax12  37234  bj-hbaeb2  37338  bj-hbnaeb  37340  bj-sbsb  37357  bj-nfcsym  37419  exlimim  37871  exellim  37873  difunieq  37903  wl-aleq  38073  wl-equsal1i  38082  wl-sb8t  38090  wl-2spsbbi  38103  wl-lem-exsb  38104  wl-lem-moexsb  38106  wl-mo2tf  38109  wl-eutf  38111  wl-mo2t  38113  wl-mo3t  38114  wl-sb8eut  38116  mopickr  38905  prtlem14  39533  axc5  39552  setindtr  43636  unielss  43830  ismnushort  44896  pm11.57  44984  pm11.59  44986  axc5c4c711toc7  44999  axc5c4c711to11  45000  axc11next  45001  ssralv2  45125  19.41rg  45144  hbexg  45150  ax6e2ndeq  45153  ssralv2VD  45459  19.41rgVD  45495  hbimpgVD  45497  hbexgVD  45499  ax6e2eqVD  45500  ax6e2ndeqVD  45502  vk15.4jVD  45507  ax6e2ndeqALT  45524  quantgodel  47473  rexsb  47718  ichnfimlem  48094  setrec1lem4  50346