Theorem sp 2220

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 39920 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 2218	. . 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  2221  sps  2222  2sp  2223  spsd  2224  19.21bi  2226  19.3t  2238  19.3  2239  19.9d  2240  sb4av  2280  sbequ2  2285  axc16gb  2297  axc7  2348  axc4  2352  19.12  2358  exsb  2389  ax12  2453  ax12b  2454  ax13ALT  2455  hbae  2461  sb4a  2510  dfsb2  2523  nfsb4t  2529  mo3  2590  mopick  2651  axi4  2724  axi5r  2725  nfcrALT  2914  rsp  3251  ceqex  3606  elrab3t  3644  abidnf  3660  mob2  3673  sbcnestgfw  4379  sbcnestgf  4384  ralidm  4473  mpteq12f  5190  axrep2  5235  axnulALT  5258  eusv1  5353  alxfr  5369  iota1  6516  dffv2  6978  fiint  9311  setrec1lem4  9964  isf32lem9  10432  nd3  10667  axrepnd  10672  axpowndlem2  10676  axpowndlem3  10677  axacndlem4  10688  trclfvcotr  15155  relexpindlem  15209  fiinopn  23212  ex-natded9.26-2  31014  bnj1294  35440  bnj570  35528  bnj953  35562  bnj1204  35635  bnj1388  35656  axsepg4  35794  in-ax8  36993  ss-ax8  36994  mh-setindnd  37305  bj-ssbid2ALT  37542  bj-sb  37569  bj-spst  37571  bj-19.21bit  37572  bj-hbext  37593  bj-substax12  37606  bj-hbaeb2  37710  bj-hbnaeb  37712  bj-sbsb  37729  bj-nfcsym  37791  exlimim  38245  exellim  38247  difunieq  38277  wl-aleq  38447  wl-equsal1i  38456  wl-sb8t  38464  wl-2spsbbi  38477  wl-lem-exsb  38478  wl-lem-moexsb  38480  wl-mo2tf  38483  wl-eutf  38485  wl-mo2t  38487  wl-mo3t  38488  wl-sb8eut  38490  findcard4  38612  mopickr  39283  prtlem14  39911  axc5  39930  setindtr  44010  unielss  44204  ismnushort  45270  pm11.57  45358  pm11.59  45360  axc5c4c711toc7  45373  axc5c4c711to11  45374  axc11next  45375  ssralv2  45499  19.41rg  45518  hbexg  45524  ax6e2ndeq  45527  ssralv2VD  45833  19.41rgVD  45869  hbimpgVD  45871  hbexgVD  45873  ax6e2eqVD  45874  ax6e2ndeqVD  45876  vk15.4jVD  45881  ax6e2ndeqALT  45898  quantgodel  47853  rexsb  48138  ichnfimlem  48514