Theorem sp 2167

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

This theorem shows that our obsolete axiom ax-c5 35039 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 2163. It is thought the best we can do using only Tarski's axioms is spw 2084. (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 1869	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		19.8a 2166	. . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
3	2	con1i 147	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑)
4	1, 3	sylbi 209	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1599  ∃wex 1823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-12 2163

This theorem depends on definitions:  df-bi 199  df-ex 1824

This theorem is referenced by:  spi  2168  sps  2169  2sp  2170  spsd  2171  19.21bi  2173  19.3t  2185  19.3  2186  19.9d  2187  19.9dOLDOLD  2188  axc16gb  2235  sb2v  2243  sb56  2248  spsbimv  2283  axc7  2292  axc4  2296  axc7eOLD  2298  19.12  2303  exsb  2327  ax12  2389  ax12b  2390  ax13ALT  2391  hbae  2397  sb2  2427  dfsb2  2449  sbequi  2451  nfsb4t  2465  exsbOLD  2548  mo3  2580  mo3OLD  2581  mopick  2662  axi4  2743  axi5r  2744  nfcr  2924  rsp  3111  ceqex  3536  elrab3t  3571  abidnf  3585  mob2  3598  sbcbi2  3705  sbcnestgf  4220  mpteq12f  4967  axrep2  5009  axnulALT  5023  dtru  5082  eusv1  5103  alxfr  5119  iota1  6113  dffv2  6531  fiint  8525  isf32lem9  9518  nd3  9746  axrepnd  9751  axpowndlem2  9755  axpowndlem3  9756  axacndlem4  9767  trclfvcotr  14157  relexpindlem  14210  fiinopn  21113  ex-natded9.26-2  27852  bnj1294  31487  bnj570  31574  bnj953  31608  bnj1204  31679  bnj1388  31700  frmin  32331  bj-hbxfrbi  33187  bj-ssbft  33232  bj-ssbequ2  33233  bj-ssbid2ALT  33236  bj-sb  33266  bj-spst  33268  bj-19.21bit  33269  bj-axrep2  33366  bj-dtru  33373  bj-hbaeb2  33380  bj-hbnaeb  33382  bj-sbsb  33399  bj-nfcsym  33457  exlimim  33785  exellim  33787  wl-aleq  33916  wl-equsal1i  33923  wl-sb8t  33928  wl-lem-exsb  33942  wl-lem-moexsb  33944  wl-mo2tf  33947  wl-eutf  33949  wl-mo2t  33951  wl-mo3t  33952  wl-sb8eut  33953  wl-ax11-lem2  33957  nfbii2OLD  34591  prtlem14  35030  axc5  35049  setindtr  38554  pm11.57  39549  pm11.59  39551  axc5c4c711toc7  39564  axc5c4c711to11  39565  axc11next  39566  iotain  39577  eubiOLD  39596  ssralv2  39695  19.41rg  39714  hbexg  39720  ax6e2ndeq  39723  ssralv2VD  40039  19.41rgVD  40075  hbimpgVD  40077  hbexgVD  40079  ax6e2eqVD  40080  ax6e2ndeqVD  40082  vk15.4jVD  40087  ax6e2ndeqALT  40104  rexsb  42131  setrec1lem4  43546