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

This theorem shows that our obsolete axiom ax-c5 38849 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 2034. Also see spvw 1981 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 1826	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		19.8a 2182	. . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
3	2	con1i 147	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑)
4	1, 3	sylbi 217	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1538  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

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

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  2316  axc4  2320  19.12  2326  exsb  2357  ax12  2421  ax12b  2422  ax13ALT  2423  hbae  2429  sb4a  2478  dfsb2  2491  nfsb4t  2497  mo3  2557  mopick  2618  axi4  2692  axi5r  2693  nfcrALT  2882  rsp  3223  ceqex  3615  elrab3t  3655  abidnf  3670  mob2  3683  sbcnestgfw  4380  sbcnestgf  4385  ralidm  4471  mpteq12f  5187  axrep2  5232  axnulALT  5254  eusv1  5341  alxfr  5357  axprlem4OLD  5379  axprlem5OLD  5380  iota1  6476  dffv2  6938  fiint  9253  fiintOLD  9254  isf32lem9  10290  nd3  10518  axrepnd  10523  axpowndlem2  10527  axpowndlem3  10528  axacndlem4  10539  trclfvcotr  14951  relexpindlem  15005  fiinopn  22764  ex-natded9.26-2  30322  bnj1294  34780  bnj570  34868  bnj953  34902  bnj1204  34975  bnj1388  34996  in-ax8  36185  ss-ax8  36186  bj-ssbid2ALT  36624  bj-sb  36648  bj-spst  36650  bj-19.21bit  36651  bj-substax12  36682  bj-hbaeb2  36779  bj-hbnaeb  36781  bj-sbsb  36798  bj-nfcsym  36860  exlimim  37303  exellim  37305  difunieq  37335  wl-aleq  37496  wl-equsal1i  37505  wl-sb8t  37513  wl-2spsbbi  37526  wl-lem-exsb  37527  wl-lem-moexsb  37529  wl-mo2tf  37532  wl-eutf  37534  wl-mo2t  37536  wl-mo3t  37537  wl-sb8eut  37539  wl-ax11-lem2  37547  mopickr  38318  prtlem14  38840  axc5  38859  setindtr  42986  unielss  43180  ismnushort  44263  pm11.57  44351  pm11.59  44353  axc5c4c711toc7  44366  axc5c4c711to11  44367  axc11next  44368  eubiOLD  44398  ssralv2  44494  19.41rg  44513  hbexg  44519  ax6e2ndeq  44522  ssralv2VD  44828  19.41rgVD  44864  hbimpgVD  44866  hbexgVD  44868  ax6e2eqVD  44869  ax6e2ndeqVD  44871  vk15.4jVD  44876  ax6e2ndeqALT  44893  rexsb  47073  ichnfimlem  47437  setrec1lem4  49652