Theorem sp 2184

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

This theorem shows that our obsolete axiom ax-c5 38839 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 2178. It is thought the best we can do using only Tarski's axioms is spw 2033. Also see spvw 1980 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 1824	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		19.8a 2182	. . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
3	2	con1i 147	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑)
4	1, 3	sylbi 217	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1535  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1778

This theorem is referenced by:  spi  2185  sps  2186  2sp  2187  spsd  2188  19.21bi  2190  19.3t  2202  19.3  2203  19.9d  2204  sb4av  2245  sbequ2  2250  axc16gb  2263  axc7  2321  axc4  2325  19.12  2331  exsb  2365  ax12  2431  ax12b  2432  ax13ALT  2433  hbae  2439  sb4a  2488  dfsb2  2501  nfsb4t  2507  mo3  2567  mopick  2628  axi4  2702  axi5r  2703  nfcrALT  2899  nfabdwOLD  2933  rsp  3253  ceqex  3665  elrab3t  3707  abidnf  3724  mob2  3737  sbcnestgfw  4444  sbcnestgf  4449  ralidm  4535  mpteq12f  5254  axrep2  5306  axnulALT  5322  eusv1  5409  alxfr  5425  axprlem4  5444  axprlem5  5445  iota1  6550  dffv2  7017  fiint  9394  fiintOLD  9395  isf32lem9  10430  nd3  10658  axrepnd  10663  axpowndlem2  10667  axpowndlem3  10668  axacndlem4  10679  trclfvcotr  15058  relexpindlem  15112  fiinopn  22928  ex-natded9.26-2  30452  bnj1294  34793  bnj570  34881  bnj953  34915  bnj1204  34988  bnj1388  35009  in-ax8  36190  ss-ax8  36191  bj-ssbid2ALT  36629  bj-sb  36653  bj-spst  36655  bj-19.21bit  36656  bj-substax12  36687  bj-hbaeb2  36784  bj-hbnaeb  36786  bj-sbsb  36803  bj-nfcsym  36865  exlimim  37308  exellim  37310  difunieq  37340  wl-aleq  37489  wl-equsal1i  37498  wl-sb8t  37506  wl-2spsbbi  37519  wl-lem-exsb  37520  wl-lem-moexsb  37522  wl-mo2tf  37525  wl-eutf  37527  wl-mo2t  37529  wl-mo3t  37530  wl-sb8eut  37532  wl-ax11-lem2  37540  mopickr  38319  prtlem14  38830  axc5  38849  setindtr  42981  unielss  43179  ismnushort  44270  pm11.57  44358  pm11.59  44360  axc5c4c711toc7  44373  axc5c4c711to11  44374  axc11next  44375  eubiOLD  44405  ssralv2  44502  19.41rg  44521  hbexg  44527  ax6e2ndeq  44530  ssralv2VD  44837  19.41rgVD  44873  hbimpgVD  44875  hbexgVD  44877  ax6e2eqVD  44878  ax6e2ndeqVD  44880  vk15.4jVD  44885  ax6e2ndeqALT  44902  rexsb  47014  ichnfimlem  47337  setrec1lem4  48782