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 39343 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  3595  elrab3t  3634  abidnf  3649  mob2  3662  sbcnestgfw  4362  sbcnestgf  4367  ralidm  4458  mpteq12f  5171  axrep2  5215  axnulALT  5239  eusv1  5328  alxfr  5344  axprlem4OLD  5367  axprlem5OLD  5368  iota1  6471  dffv2  6929  fiint  9230  isf32lem9  10274  nd3  10503  axrepnd  10508  axpowndlem2  10512  axpowndlem3  10513  axacndlem4  10524  trclfvcotr  14962  relexpindlem  15016  fiinopn  22876  ex-natded9.26-2  30505  bnj1294  34975  bnj570  35063  bnj953  35097  bnj1204  35170  bnj1388  35191  in-ax8  36422  ss-ax8  36423  mh-setindnd  36735  bj-ssbid2ALT  36973  bj-sb  37000  bj-spst  37002  bj-19.21bit  37003  bj-hbext  37024  bj-substax12  37037  bj-hbaeb2  37141  bj-hbnaeb  37143  bj-sbsb  37160  bj-nfcsym  37222  exlimim  37672  exellim  37674  difunieq  37704  wl-aleq  37874  wl-equsal1i  37883  wl-sb8t  37891  wl-2spsbbi  37904  wl-lem-exsb  37905  wl-lem-moexsb  37907  wl-mo2tf  37910  wl-eutf  37912  wl-mo2t  37914  wl-mo3t  37915  wl-sb8eut  37917  mopickr  38706  prtlem14  39334  axc5  39353  setindtr  43470  unielss  43664  ismnushort  44746  pm11.57  44834  pm11.59  44836  axc5c4c711toc7  44849  axc5c4c711to11  44850  axc11next  44851  ssralv2  44976  19.41rg  44995  hbexg  45001  ax6e2ndeq  45004  ssralv2VD  45310  19.41rgVD  45346  hbimpgVD  45348  hbexgVD  45350  ax6e2eqVD  45351  ax6e2ndeqVD  45353  vk15.4jVD  45358  ax6e2ndeqALT  45375  rexsb  47559  ichnfimlem  47935  setrec1lem4  50177