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

This theorem shows that our obsolete axiom ax-c5 39756 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 2067. Also see spvw 2014 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 1859	. 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 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-ex 1813

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  2279  sbequ2  2284  axc16gb  2296  axc7  2347  axc4  2351  19.12  2357  exsb  2388  ax12  2452  ax12b  2453  ax13ALT  2454  hbae  2460  sb4a  2509  dfsb2  2522  nfsb4t  2528  mo3  2589  mopick  2650  axi4  2723  axi5r  2724  nfcrALT  2913  rsp  3250  ceqex  3606  elrab3t  3644  abidnf  3660  mob2  3673  sbcnestgfw  4379  sbcnestgf  4384  ralidm  4473  mpteq12f  5190  axrep2  5235  axnulALT  5261  eusv1  5356  alxfr  5372  axprlem4OLD  5395  axprlem5OLD  5396  iota1  6512  dffv2  6973  fiint  9296  isf32lem9  10363  nd3  10598  axrepnd  10603  axpowndlem2  10607  axpowndlem3  10608  axacndlem4  10619  trclfvcotr  15082  relexpindlem  15136  fiinopn  23126  ex-natded9.26-2  30900  bnj1294  35326  bnj570  35414  bnj953  35448  bnj1204  35521  bnj1388  35542  axsepg4  35669  in-ax8  36844  ss-ax8  36845  mh-setindnd  37156  bj-ssbid2ALT  37393  bj-sb  37420  bj-spst  37422  bj-19.21bit  37423  bj-hbext  37444  bj-substax12  37457  bj-hbaeb2  37561  bj-hbnaeb  37563  bj-sbsb  37580  bj-nfcsym  37642  exlimim  38096  exellim  38098  difunieq  38128  wl-aleq  38298  wl-equsal1i  38307  wl-sb8t  38315  wl-2spsbbi  38328  wl-lem-exsb  38329  wl-lem-moexsb  38331  wl-mo2tf  38334  wl-eutf  38336  wl-mo2t  38338  wl-mo3t  38339  wl-sb8eut  38341  findcard4  38463  mopickr  39119  prtlem14  39747  axc5  39766  setindtr  43865  unielss  44059  ismnushort  45125  pm11.57  45213  pm11.59  45215  axc5c4c711toc7  45228  axc5c4c711to11  45229  axc11next  45230  ssralv2  45354  19.41rg  45373  hbexg  45379  ax6e2ndeq  45382  ssralv2VD  45688  19.41rgVD  45724  hbimpgVD  45726  hbexgVD  45728  ax6e2eqVD  45729  ax6e2ndeqVD  45731  vk15.4jVD  45736  ax6e2ndeqALT  45753  quantgodel  47702  rexsb  47987  ichnfimlem  48363  setrec1lem4  50616