Theorem sp 2190

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 39143 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 2184. 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 2188	. . 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 2184

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

This theorem is referenced by:  spi  2191  sps  2192  2sp  2193  spsd  2194  19.21bi  2196  19.3t  2208  19.3  2209  19.9d  2210  sb4av  2251  sbequ2  2256  axc16gb  2269  axc7  2322  axc4  2326  19.12  2332  exsb  2363  ax12  2427  ax12b  2428  ax13ALT  2429  hbae  2435  sb4a  2484  dfsb2  2497  nfsb4t  2503  mo3  2564  mopick  2625  axi4  2699  axi5r  2700  nfcrALT  2889  rsp  3224  ceqex  3606  elrab3t  3645  abidnf  3660  mob2  3673  sbcnestgfw  4373  sbcnestgf  4378  ralidm  4470  mpteq12f  5183  axrep2  5227  axnulALT  5249  eusv1  5336  alxfr  5352  axprlem4OLD  5374  axprlem5OLD  5375  iota1  6471  dffv2  6929  fiint  9227  isf32lem9  10271  nd3  10500  axrepnd  10505  axpowndlem2  10509  axpowndlem3  10510  axacndlem4  10521  trclfvcotr  14932  relexpindlem  14986  fiinopn  22845  ex-natded9.26-2  30495  bnj1294  34973  bnj570  35061  bnj953  35095  bnj1204  35168  bnj1388  35189  in-ax8  36418  ss-ax8  36419  mh-setindnd  36667  bj-ssbid2ALT  36864  bj-sb  36888  bj-spst  36890  bj-19.21bit  36891  bj-substax12  36922  bj-hbaeb2  37019  bj-hbnaeb  37021  bj-sbsb  37038  bj-nfcsym  37100  exlimim  37547  exellim  37549  difunieq  37579  wl-aleq  37740  wl-equsal1i  37749  wl-sb8t  37757  wl-2spsbbi  37770  wl-lem-exsb  37771  wl-lem-moexsb  37773  wl-mo2tf  37776  wl-eutf  37778  wl-mo2t  37780  wl-mo3t  37781  wl-sb8eut  37783  mopickr  38556  prtlem14  39134  axc5  39153  setindtr  43266  unielss  43460  ismnushort  44542  pm11.57  44630  pm11.59  44632  axc5c4c711toc7  44645  axc5c4c711to11  44646  axc11next  44647  ssralv2  44772  19.41rg  44791  hbexg  44797  ax6e2ndeq  44800  ssralv2VD  45106  19.41rgVD  45142  hbimpgVD  45144  hbexgVD  45146  ax6e2eqVD  45147  ax6e2ndeqVD  45149  vk15.4jVD  45154  ax6e2ndeqALT  45171  rexsb  47345  ichnfimlem  47709  setrec1lem4  49935