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 39685 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 ⊢ (∀𝑥𝜑 → 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1568  ∃wex 1809

This proof depends on 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 proof depends on definitions:  df-bi 210  df-ex 1810

This theorem is used 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  3611  elrab3t  3649  abidnf  3665  mob2  3678  sbcnestgfw  4386  sbcnestgf  4391  ralidm  4478  mpteq12f  5196  axrep2  5241  axnulALT  5267  eusv1  5362  alxfr  5378  axprlem4OLD  5401  axprlem5OLD  5402  iota1  6515  dffv2  6976  fiint  9282  isf32lem9  10349  nd3  10578  axrepnd  10583  axpowndlem2  10587  axpowndlem3  10588  axacndlem4  10599  trclfvcotr  15051  relexpindlem  15105  fiinopn  23067  ex-natded9.26-2  30780  bnj1294  35214  bnj570  35302  bnj953  35336  bnj1204  35409  bnj1388  35430  axsepg4  35564  in-ax8  36764  ss-ax8  36765  mh-setindnd  37076  bj-ssbid2ALT  37313  bj-sb  37340  bj-spst  37342  bj-19.21bit  37343  bj-hbext  37364  bj-substax12  37377  bj-hbaeb2  37481  bj-hbnaeb  37483  bj-sbsb  37500  bj-nfcsym  37562  exlimim  38016  exellim  38018  difunieq  38048  wl-aleq  38218  wl-equsal1i  38227  wl-sb8t  38235  wl-2spsbbi  38248  wl-lem-exsb  38249  wl-lem-moexsb  38251  wl-mo2tf  38254  wl-eutf  38256  wl-mo2t  38258  wl-mo3t  38259  wl-sb8eut  38261  mopickr  39048  prtlem14  39676  axc5  39695  setindtr  43779  unielss  43973  ismnushort  45039  pm11.57  45127  pm11.59  45129  axc5c4c711toc7  45142  axc5c4c711to11  45143  axc11next  45144  ssralv2  45268  19.41rg  45287  hbexg  45293  ax6e2ndeq  45296  ssralv2VD  45602  19.41rgVD  45638  hbimpgVD  45640  hbexgVD  45642  ax6e2eqVD  45643  ax6e2ndeqVD  45645  vk15.4jVD  45650  ax6e2ndeqALT  45667  quantgodel  47616  rexsb  47864  ichnfimlem  48240  setrec1lem4  50496