Theorem sp 2191

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

This theorem shows that our obsolete axiom ax-c5 39256 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 2185. It is thought the best we can do using only Tarski's axioms is spw 2036. Also see spvw 1983 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 1828	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		19.8a 2189	. . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
3	2	con1i 147	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑)
4	1, 3	sylbi 217	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1540  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  spi  2192  sps  2193  2sp  2194  spsd  2195  19.21bi  2197  19.3t  2209  19.3  2210  19.9d  2211  sb4av  2252  sbequ2  2257  axc16gb  2270  axc7  2323  axc4  2327  19.12  2333  exsb  2364  ax12  2428  ax12b  2429  ax13ALT  2430  hbae  2436  sb4a  2485  dfsb2  2498  nfsb4t  2504  mo3  2565  mopick  2626  axi4  2700  axi5r  2701  nfcrALT  2890  rsp  3226  ceqex  3608  elrab3t  3647  abidnf  3662  mob2  3675  sbcnestgfw  4375  sbcnestgf  4380  ralidm  4472  mpteq12f  5185  axrep2  5229  axnulALT  5251  eusv1  5338  alxfr  5354  axprlem4OLD  5376  axprlem5OLD  5377  iota1  6479  dffv2  6937  fiint  9239  isf32lem9  10283  nd3  10512  axrepnd  10517  axpowndlem2  10521  axpowndlem3  10522  axacndlem4  10533  trclfvcotr  14944  relexpindlem  14998  fiinopn  22857  ex-natded9.26-2  30507  bnj1294  34992  bnj570  35080  bnj953  35114  bnj1204  35187  bnj1388  35208  in-ax8  36437  ss-ax8  36438  mh-setindnd  36686  bj-ssbid2ALT  36905  bj-sb  36929  bj-spst  36931  bj-19.21bit  36932  bj-substax12  36964  bj-hbaeb2  37063  bj-hbnaeb  37065  bj-sbsb  37082  bj-nfcsym  37144  exlimim  37594  exellim  37596  difunieq  37626  wl-aleq  37787  wl-equsal1i  37796  wl-sb8t  37804  wl-2spsbbi  37817  wl-lem-exsb  37818  wl-lem-moexsb  37820  wl-mo2tf  37823  wl-eutf  37825  wl-mo2t  37827  wl-mo3t  37828  wl-sb8eut  37830  mopickr  38619  prtlem14  39247  axc5  39266  setindtr  43378  unielss  43572  ismnushort  44654  pm11.57  44742  pm11.59  44744  axc5c4c711toc7  44757  axc5c4c711to11  44758  axc11next  44759  ssralv2  44884  19.41rg  44903  hbexg  44909  ax6e2ndeq  44912  ssralv2VD  45218  19.41rgVD  45254  hbimpgVD  45256  hbexgVD  45258  ax6e2eqVD  45259  ax6e2ndeqVD  45261  vk15.4jVD  45266  ax6e2ndeqALT  45283  rexsb  47456  ichnfimlem  47820  setrec1lem4  50046