Theorem sp 2219

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

This theorem shows that our obsolete axiom ax-c5 39638 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 2213. It is thought the best we can do using only Tarski's axioms is spw 2064. Also see spvw 2011 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 1856	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		19.8a 2217	. . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
3	2	con1i 148	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑)
4	1, 3	sylbi 220	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1568  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  spi  2220  sps  2221  2sp  2222  spsd  2223  19.21bi  2225  19.3t  2237  19.3  2238  19.9d  2239  sb4av  2280  sbequ2  2285  axc16gb  2298  axc7  2350  axc4  2354  19.12  2360  exsb  2391  ax12  2455  ax12b  2456  ax13ALT  2457  hbae  2463  sb4a  2512  dfsb2  2525  nfsb4t  2531  mo3  2592  mopick  2653  axi4  2726  axi5r  2727  nfcrALT  2916  rsp  3253  ceqex  3612  elrab3t  3650  abidnf  3666  mob2  3679  sbcnestgfw  4387  sbcnestgf  4392  ralidm  4479  mpteq12f  5197  axrep2  5242  axnulALT  5268  eusv1  5364  alxfr  5380  axprlem4OLD  5403  axprlem5OLD  5404  iota1  6517  dffv2  6978  fiint  9287  isf32lem9  10346  nd3  10575  axrepnd  10580  axpowndlem2  10584  axpowndlem3  10585  axacndlem4  10596  trclfvcotr  15048  relexpindlem  15102  fiinopn  23039  ex-natded9.26-2  30752  bnj1294  35186  bnj570  35274  bnj953  35308  bnj1204  35381  bnj1388  35402  axsepg4  35537  in-ax8  36717  ss-ax8  36718  mh-setindnd  37029  bj-ssbid2ALT  37266  bj-sb  37293  bj-spst  37295  bj-19.21bit  37296  bj-hbext  37317  bj-substax12  37330  bj-hbaeb2  37434  bj-hbnaeb  37436  bj-sbsb  37453  bj-nfcsym  37515  exlimim  37969  exellim  37971  difunieq  38001  wl-aleq  38171  wl-equsal1i  38180  wl-sb8t  38188  wl-2spsbbi  38201  wl-lem-exsb  38202  wl-lem-moexsb  38204  wl-mo2tf  38207  wl-eutf  38209  wl-mo2t  38211  wl-mo3t  38212  wl-sb8eut  38214  mopickr  39001  prtlem14  39629  axc5  39648  setindtr  43734  unielss  43928  ismnushort  44994  pm11.57  45082  pm11.59  45084  axc5c4c711toc7  45097  axc5c4c711to11  45098  axc11next  45099  ssralv2  45223  19.41rg  45242  hbexg  45248  ax6e2ndeq  45251  ssralv2VD  45557  19.41rgVD  45593  hbimpgVD  45595  hbexgVD  45597  ax6e2eqVD  45598  ax6e2ndeqVD  45600  vk15.4jVD  45605  ax6e2ndeqALT  45622  quantgodel  47571  rexsb  47819  ichnfimlem  48195  setrec1lem4  50451