Theorem sp 2177

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 36904 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 2172. 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 2175	. . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
3	2	con1i 147	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑)
4	1, 3	sylbi 216	1 ⊢ (∀𝑥𝜑 → 𝜑)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

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

This theorem is referenced by:  spi  2178  sps  2179  2sp  2180  spsd  2181  19.21bi  2183  19.3t  2195  19.3  2196  19.9d  2197  sb4av  2237  sbequ2  2242  sbequ2OLD  2243  axc16gb  2255  axc7  2312  axc4  2316  19.12  2322  exsb  2358  ax12  2424  ax12b  2425  ax13ALT  2426  hbae  2432  sb4a  2485  dfsb2  2498  nfsb4t  2504  mo3  2565  mopick  2628  axi4  2701  axi5r  2702  nfcrALT  2894  nfcriOLDOLD  2899  nfabdwOLD  2932  rsp  3132  ceqex  3583  elrab3t  3624  abidnf  3639  mob2  3651  sbcbi2OLD  3780  sbcnestgfw  4353  sbcnestgf  4358  ralidm  4443  mpteq12f  5163  axrep2  5213  axnulALT  5229  eusv1  5315  alxfr  5331  axprlem4  5350  axprlem5  5351  iota1  6414  dffv2  6872  fiint  9100  isf32lem9  10126  nd3  10354  axrepnd  10359  axpowndlem2  10363  axpowndlem3  10364  axacndlem4  10375  trclfvcotr  14729  relexpindlem  14783  fiinopn  22059  ex-natded9.26-2  28793  bnj1294  32806  bnj570  32894  bnj953  32928  bnj1204  33001  bnj1388  33022  bj-ssbid2ALT  34853  bj-sb  34878  bj-spst  34880  bj-19.21bit  34881  bj-substax12  34912  bj-dtru  35008  bj-hbaeb2  35010  bj-hbnaeb  35012  bj-sbsb  35029  bj-nfcsym  35093  exlimim  35522  exellim  35524  difunieq  35554  wl-aleq  35703  wl-equsal1i  35711  wl-sb8t  35716  wl-2spsbbi  35729  wl-lem-exsb  35730  wl-lem-moexsb  35732  wl-mo2tf  35735  wl-eutf  35737  wl-mo2t  35739  wl-mo3t  35740  wl-sb8eut  35741  wl-ax11-lem2  35746  prtlem14  36895  axc5  36914  setindtr  40853  ismnushort  41926  pm11.57  42014  pm11.59  42016  axc5c4c711toc7  42029  axc5c4c711to11  42030  axc11next  42031  eubiOLD  42061  ssralv2  42158  19.41rg  42177  hbexg  42183  ax6e2ndeq  42186  ssralv2VD  42493  19.41rgVD  42529  hbimpgVD  42531  hbexgVD  42533  ax6e2eqVD  42534  ax6e2ndeqVD  42536  vk15.4jVD  42541  ax6e2ndeqALT  42558  rexsb  44602  ichnfimlem  44926  setrec1lem4  46407