Theorem sp 2091

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

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1521  ∃wex 1744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087

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

This theorem is referenced by:  spi  2092  sps  2093  2sp  2094  spsd  2095  19.21bi  2097  19.3  2107  19.9d  2108  axc4  2168  axc7  2170  axc7e  2171  axc16gb  2174  sb56  2188  19.12  2200  nfaldOLD  2202  nfrOLD  2224  19.3OLD  2238  ax12  2340  ax13ALT  2341  hbae  2348  ax12OLD  2372  ax12b  2373  sb2  2380  dfsb2  2401  sbequi  2403  nfsb4t  2417  exsb  2496  mo3  2536  mopick  2564  axi4  2622  axi5r  2623  nfcr  2785  rsp  2958  ceqex  3364  elrab3t  3395  abidnf  3408  mob2  3419  sbcnestgf  4028  mpteq12f  4764  axrep2  4806  axnulALT  4820  dtru  4887  eusv1  4890  alxfr  4908  iota1  5903  dffv2  6310  fiint  8278  isf32lem9  9221  nd3  9449  axrepnd  9454  axpowndlem2  9458  axpowndlem3  9459  axacndlem4  9470  trclfvcotr  13794  relexpindlem  13847  fiinopn  20754  ex-natded9.26-2  27407  bnj1294  31014  bnj570  31101  bnj953  31135  bnj1204  31206  bnj1388  31227  frmin  31867  bj-hbxfrbi  32733  bj-ssbft  32767  bj-ssbequ2  32768  bj-ssbid2ALT  32771  bj-sb  32802  bj-spst  32804  bj-19.21bit  32805  bj-19.3t  32814  bj-sb2v  32878  bj-axrep2  32914  bj-dtru  32922  bj-hbaeb2  32930  bj-hbnaeb  32932  bj-sbsb  32949  bj-nfcsym  33011  exlimim  33319  exellim  33322  wl-aleq  33452  wl-equsal1i  33459  wl-sb8t  33463  wl-lem-exsb  33478  wl-lem-moexsb  33480  wl-mo2tf  33483  wl-eutf  33485  wl-mo2t  33487  wl-mo3t  33488  wl-sb8eut  33489  wl-ax11-lem2  33493  nfbii2  34097  prtlem14  34478  axc5  34497  setindtr  37908  pm11.57  38906  pm11.59  38908  axc5c4c711toc7  38922  axc5c4c711to11  38923  axc11next  38924  iotain  38935  eubi  38954  ssralv2  39054  19.41rg  39083  hbexg  39089  ax6e2ndeq  39092  ssralv2VD  39416  19.41rgVD  39452  hbimpgVD  39454  hbexgVD  39456  ax6e2eqVD  39457  ax6e2ndeqVD  39459  vk15.4jVD  39464  ax6e2ndeqALT  39481  rexsb  41489  setrec1lem4  42762