Theorem sp 2178

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

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1537  ∃wex 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-ex 1784

This theorem is referenced by:  spi  2179  sps  2180  2sp  2181  spsd  2182  19.21bi  2184  19.3t  2197  19.3  2198  19.9d  2199  sb4av  2239  sbequ2  2244  sbequ2OLD  2245  axc16gb  2257  axc7  2315  axc4  2319  19.12  2325  exsb  2357  ax12  2423  ax12b  2424  ax13ALT  2425  hbae  2431  sb4a  2484  dfsb2  2497  nfsb4t  2503  mo3  2564  mopick  2627  axi4  2700  axi5r  2701  nfcrALT  2892  nfcriOLDOLD  2897  nfabdwOLD  2930  rsp  3129  ceqex  3574  elrab3t  3616  abidnf  3633  mob2  3645  sbcbi2OLD  3775  sbcnestgfw  4349  sbcnestgf  4354  ralidm  4439  mpteq12f  5158  axrep2  5208  axnulALT  5223  eusv1  5309  alxfr  5325  axprlem4  5344  axprlem5  5345  iota1  6395  dffv2  6845  fiint  9021  frmin  9438  isf32lem9  10048  nd3  10276  axrepnd  10281  axpowndlem2  10285  axpowndlem3  10286  axacndlem4  10297  trclfvcotr  14648  relexpindlem  14702  fiinopn  21958  ex-natded9.26-2  28685  bnj1294  32697  bnj570  32785  bnj953  32819  bnj1204  32892  bnj1388  32913  bj-ssbid2ALT  34771  bj-sb  34796  bj-spst  34798  bj-19.21bit  34799  bj-substax12  34830  bj-dtru  34926  bj-hbaeb2  34928  bj-hbnaeb  34930  bj-sbsb  34947  bj-nfcsym  35011  exlimim  35440  exellim  35442  difunieq  35472  wl-aleq  35621  wl-equsal1i  35629  wl-sb8t  35634  wl-2spsbbi  35647  wl-lem-exsb  35648  wl-lem-moexsb  35650  wl-mo2tf  35653  wl-eutf  35655  wl-mo2t  35657  wl-mo3t  35658  wl-sb8eut  35659  wl-ax11-lem2  35664  prtlem14  36815  axc5  36834  setindtr  40762  ismnushort  41808  pm11.57  41896  pm11.59  41898  axc5c4c711toc7  41911  axc5c4c711to11  41912  axc11next  41913  eubiOLD  41943  ssralv2  42040  19.41rg  42059  hbexg  42065  ax6e2ndeq  42068  ssralv2VD  42375  19.41rgVD  42411  hbimpgVD  42413  hbexgVD  42415  ax6e2eqVD  42416  ax6e2ndeqVD  42418  vk15.4jVD  42423  ax6e2ndeqALT  42440  rexsb  44478  ichnfimlem  44803  setrec1lem4  46282