Theorem sp 2222

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 39690 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 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 2220	. . 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 2216

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

This theorem is used by:  spi  2223  sps  2224  2sp  2225  spsd  2226  19.21bi  2228  19.3t  2240  19.3  2241  19.9d  2242  sb4av  2282  sbequ2  2287  axc16gb  2300  axc7  2352  axc4  2356  19.12  2362  exsb  2393  ax12  2457  ax12b  2458  ax13ALT  2459  hbae  2465  sb4a  2514  dfsb2  2527  nfsb4t  2533  mo3  2594  mopick  2655  axi4  2728  axi5r  2729  nfcrALT  2918  rsp  3255  ceqex  3613  elrab3t  3651  abidnf  3667  mob2  3680  sbcnestgfw  4386  sbcnestgf  4391  ralidm  4480  mpteq12f  5198  axrep2  5243  axnulALT  5269  eusv1  5364  alxfr  5380  axprlem4OLD  5403  axprlem5OLD  5404  iota1  6519  dffv2  6980  fiint  9289  isf32lem9  10356  nd3  10585  axrepnd  10590  axpowndlem2  10594  axpowndlem3  10595  axacndlem4  10606  trclfvcotr  15065  relexpindlem  15119  fiinopn  23087  ex-natded9.26-2  30800  bnj1294  35229  bnj570  35317  bnj953  35351  bnj1204  35424  bnj1388  35445  axsepg4  35572  in-ax8  36769  ss-ax8  36770  mh-setindnd  37081  bj-ssbid2ALT  37318  bj-sb  37345  bj-spst  37347  bj-19.21bit  37348  bj-hbext  37369  bj-substax12  37382  bj-hbaeb2  37486  bj-hbnaeb  37488  bj-sbsb  37505  bj-nfcsym  37567  exlimim  38021  exellim  38023  difunieq  38053  wl-aleq  38223  wl-equsal1i  38232  wl-sb8t  38240  wl-2spsbbi  38253  wl-lem-exsb  38254  wl-lem-moexsb  38256  wl-mo2tf  38259  wl-eutf  38261  wl-mo2t  38263  wl-mo3t  38264  wl-sb8eut  38266  mopickr  39053  prtlem14  39681  axc5  39700  setindtr  43784  unielss  43978  ismnushort  45044  pm11.57  45132  pm11.59  45134  axc5c4c711toc7  45147  axc5c4c711to11  45148  axc11next  45149  ssralv2  45273  19.41rg  45292  hbexg  45298  ax6e2ndeq  45301  ssralv2VD  45607  19.41rgVD  45643  hbimpgVD  45645  hbexgVD  45647  ax6e2eqVD  45648  ax6e2ndeqVD  45650  vk15.4jVD  45655  ax6e2ndeqALT  45672  quantgodel  47621  rexsb  47869  ichnfimlem  48245  setrec1lem4  50501