Theorem sp 2223

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

This theorem shows that our obsolete axiom ax-c5 40206 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 2216. It is thought the best we can do using only Tarski's axioms is spw 2069. Also see spvw 2016 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 2221	. . 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 1945  ax-6 2002  ax-7 2043  ax-12 2216

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

This theorem is used by:  spi  2224  sps  2225  2sp  2226  spsd  2227  19.21bi  2229  19.3t  2241  19.3  2242  19.9d  2243  sb4av  2283  sbequ2  2288  axc16gb  2300  axc7  2351  axc4  2355  19.12  2361  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  2917  rsp  3254  ceqex  3609  elrab3t  3647  abidnf  3663  mob2  3676  sbcnestgfw  4382  sbcnestgf  4387  ralidm  4476  mpteq12f  5196  axrep2  5241  axnulALT  5264  eusv1  5360  alxfr  5376  iota1  6544  dffv2  7011  fiint  9356  setrec1lem4  10008  isf32lem9  10478  nd3  10713  axrepnd  10718  axpowndlem2  10722  axpowndlem3  10723  axacndlem4  10734  trclfvcotr  15205  relexpindlem  15259  fiinopn  23274  ex-natded9.26-2  31078  bnj1294  35558  bnj570  35646  bnj953  35680  bnj1204  35753  bnj1388  35774  axsepg4  35952  in-ax8  37228  ss-ax8  37229  mh-setindnd  37540  bj-ssbid2ALT  37777  bj-sb  37804  bj-spst  37806  bj-19.21bit  37807  bj-hbext  37828  bj-substax12  37841  bj-hbaeb2  37945  bj-hbnaeb  37947  bj-sbsb  37964  bj-nfcsym  38026  exlimim  38533  exellim  38535  difunieq  38565  wl-aleq  38735  wl-equsal1i  38744  wl-sb8t  38752  wl-2spsbbi  38765  wl-lem-exsb  38766  wl-lem-moexsb  38768  wl-mo2tf  38771  wl-eutf  38773  wl-mo2t  38775  wl-mo3t  38776  wl-sb8eut  38778  findcard4  38900  mopickr  39569  prtlem14  40197  axc5  40216  setindtr  44297  unielss  44481  ismnushort  45546  pm11.57  45634  pm11.59  45636  axc5c4c711toc7  45649  axc5c4c711to11  45650  axc11next  45651  ssralv2  45774  19.41rg  45793  hbexg  45799  ax6e2ndeq  45802  ssralv2VD  46108  19.41rgVD  46144  hbimpgVD  46146  hbexgVD  46148  ax6e2eqVD  46149  ax6e2ndeqVD  46151  vk15.4jVD  46156  ax6e2ndeqALT  46173  quantgodel  48157  rexsb  48443  ichnfimlem  48818