Theorem sp 2041

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

This theorem shows that our obsolete axiom ax-c5 33186 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 2034. It is thought the best we can do using only Tarski's axioms is spw 1954. (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 1743	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		19.8a 2039	. . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
3	2	con1i 143	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑)
4	1, 3	sylbi 206	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1473  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  spi  2042  sps  2043  2sp  2044  spsd  2045  19.21bi  2047  19.3  2057  19.9d  2058  axc4  2115  axc7  2117  axc7e  2118  axc16gb  2121  sb56  2136  19.12  2150  nfaldOLD  2152  nfrOLD  2176  19.3OLD  2190  ax12  2292  ax13OLD  2293  hbae  2303  ax12OLD  2329  ax12b  2333  sb2  2340  dfsb2  2361  sbequi  2363  nfsb4t  2377  exsb  2456  mo3  2495  mopick  2523  axi4  2581  axi5r  2582  nfcr  2743  rsp  2913  ceqex  3303  elrab3t  3330  abidnf  3342  mob2  3353  sbcnestgf  3947  mpteq12f  4661  axrep2  4701  axnulALT  4715  dtru  4783  eusv1  4786  alxfr  4804  iota1  5782  dffv2  6181  fiint  8122  isf32lem9  9066  nd3  9290  axrepnd  9295  axpowndlem2  9299  axpowndlem3  9300  axacndlem4  9311  trclfvcotr  13598  relexpindlem  13651  fiinopn  20531  ex-natded9.26-2  26669  bnj1294  30142  bnj570  30229  bnj953  30263  bnj1204  30334  bnj1388  30355  frmin  30983  bj-hbxfrbi  31792  bj-ssbft  31831  bj-ssbequ2  31832  bj-ssbid2ALT  31835  bj-sb  31864  bj-spst  31866  bj-19.21bit  31867  bj-19.3t  31876  bj-sb2v  31941  bj-axrep2  31977  bj-dtru  31985  bj-hbaeb2  31993  bj-hbnaeb  31995  bj-sbsb  32012  bj-nfcsym  32079  bj-ax9  32083  exlimim  32365  exellim  32368  wl-aleq  32501  wl-equsal1i  32508  wl-sb8t  32512  wl-lem-exsb  32527  wl-lem-moexsb  32529  wl-mo2tf  32532  wl-eutf  32534  wl-mo2t  32536  wl-mo3t  32537  wl-sb8eut  32538  wl-ax11-lem2  32542  nfbii2  33137  prtlem14  33177  axc5  33196  setindtr  36609  pm11.57  37611  pm11.59  37613  axc5c4c711toc7  37627  axc5c4c711to11  37628  axc11next  37629  iotain  37640  eubi  37659  ssralv2  37758  19.41rg  37787  hbexg  37793  ax6e2ndeq  37796  ssralv2VD  38124  19.41rgVD  38160  hbimpgVD  38162  hbexgVD  38164  ax6e2eqVD  38165  ax6e2ndeqVD  38167  vk15.4jVD  38172  ax6e2ndeqALT  38189  rexsb  39817  setrec1lem4  42236