Theorem sp 2053

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

This theorem shows that our obsolete axiom ax-c5 34168 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 2047. It is thought the best we can do using only Tarski's axioms is spw 1967. (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 1753	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		19.8a 2052	. . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
3	2	con1i 144	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑)
4	1, 3	sylbi 207	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1481  ∃wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  spi  2054  sps  2055  2sp  2056  spsd  2057  19.21bi  2059  19.3  2069  19.9d  2070  axc4  2130  axc7  2132  axc7e  2133  axc16gb  2136  sb56  2150  19.12  2164  nfaldOLD  2166  nfrOLD  2188  19.3OLD  2202  ax12  2304  ax13ALT  2305  hbae  2315  ax12OLD  2341  ax12b  2345  sb2  2352  dfsb2  2373  sbequi  2375  nfsb4t  2389  exsb  2468  mo3  2507  mopick  2535  axi4  2593  axi5r  2594  nfcr  2756  rsp  2929  ceqex  3333  elrab3t  3362  abidnf  3375  mob2  3386  sbcnestgf  3995  mpteq12f  4731  axrep2  4773  axnulALT  4787  dtru  4857  eusv1  4860  alxfr  4878  iota1  5865  dffv2  6271  fiint  8237  isf32lem9  9183  nd3  9411  axrepnd  9416  axpowndlem2  9420  axpowndlem3  9421  axacndlem4  9432  trclfvcotr  13750  relexpindlem  13803  fiinopn  20706  ex-natded9.26-2  27277  bnj1294  30888  bnj570  30975  bnj953  31009  bnj1204  31080  bnj1388  31101  frmin  31739  bj-hbxfrbi  32608  bj-ssbft  32642  bj-ssbequ2  32643  bj-ssbid2ALT  32646  bj-sb  32677  bj-spst  32679  bj-19.21bit  32680  bj-19.3t  32689  bj-sb2v  32753  bj-axrep2  32789  bj-dtru  32797  bj-hbaeb2  32805  bj-hbnaeb  32807  bj-sbsb  32824  bj-nfcsym  32886  exlimim  33189  exellim  33192  wl-aleq  33322  wl-equsal1i  33329  wl-sb8t  33333  wl-lem-exsb  33348  wl-lem-moexsb  33350  wl-mo2tf  33353  wl-eutf  33355  wl-mo2t  33357  wl-mo3t  33358  wl-sb8eut  33359  wl-ax11-lem2  33363  nfbii2  33967  prtlem14  34159  axc5  34178  setindtr  37591  pm11.57  38589  pm11.59  38591  axc5c4c711toc7  38605  axc5c4c711to11  38606  axc11next  38607  iotain  38618  eubi  38637  ssralv2  38737  19.41rg  38766  hbexg  38772  ax6e2ndeq  38775  ssralv2VD  39102  19.41rgVD  39138  hbimpgVD  39140  hbexgVD  39142  ax6e2eqVD  39143  ax6e2ndeqVD  39145  vk15.4jVD  39150  ax6e2ndeqALT  39167  rexsb  41168  setrec1lem4  42437