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 39002 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  4461  mpteq12f  5178  axrep2  5222  axnulALT  5244  eusv1  5331  alxfr  5347  axprlem4OLD  5369  axprlem5OLD  5370  iota1  6465  dffv2  6923  fiint  9218  isf32lem9  10259  nd3  10487  axrepnd  10492  axpowndlem2  10496  axpowndlem3  10497  axacndlem4  10508  trclfvcotr  14918  relexpindlem  14972  fiinopn  22817  ex-natded9.26-2  30402  bnj1294  34850  bnj570  34938  bnj953  34972  bnj1204  35045  bnj1388  35066  in-ax8  36289  ss-ax8  36290  bj-ssbid2ALT  36728  bj-sb  36752  bj-spst  36754  bj-19.21bit  36755  bj-substax12  36786  bj-hbaeb2  36883  bj-hbnaeb  36885  bj-sbsb  36902  bj-nfcsym  36964  exlimim  37407  exellim  37409  difunieq  37439  wl-aleq  37600  wl-equsal1i  37609  wl-sb8t  37617  wl-2spsbbi  37630  wl-lem-exsb  37631  wl-lem-moexsb  37633  wl-mo2tf  37636  wl-eutf  37638  wl-mo2t  37640  wl-mo3t  37641  wl-sb8eut  37643  mopickr  38415  prtlem14  38993  axc5  39012  setindtr  43141  unielss  43335  ismnushort  44418  pm11.57  44506  pm11.59  44508  axc5c4c711toc7  44521  axc5c4c711to11  44522  axc11next  44523  ssralv2  44648  19.41rg  44667  hbexg  44673  ax6e2ndeq  44676  ssralv2VD  44982  19.41rgVD  45018  hbimpgVD  45020  hbexgVD  45022  ax6e2eqVD  45023  ax6e2ndeqVD  45025  vk15.4jVD  45030  ax6e2ndeqALT  45047  rexsb  47223  ichnfimlem  47587  setrec1lem4  49815