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

This theorem shows that our obsolete axiom ax-c5 36013 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 2037. 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 1822	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		19.8a 2176	. . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
3	2	con1i 149	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑)
4	1, 3	sylbi 219	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1531  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-12 2173

This theorem depends on definitions:  df-bi 209  df-ex 1777

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  2240  sbequ2  2246  sbequ2OLD  2247  axc16gb  2259  sb56OLD  2274  spsbimvOLD  2324  axc7  2332  axc4  2336  19.12  2342  exsb  2374  ax12  2441  ax12b  2442  ax13ALT  2443  hbae  2449  sb4a  2505  sb2vOLDOLD  2508  dfsb2  2528  sbequiOLD  2530  nfsb4t  2535  sb2vOLDALT  2579  sb2ALT  2583  dfsb2ALT  2587  sbequiALT  2592  nfsb4tALT  2600  mo3  2644  mopick  2706  axi4  2782  axi5r  2783  nfcr  2966  nfabdw  3000  rsp  3205  ceqex  3644  elrab3t  3678  abidnf  3693  mob2  3705  sbcbi2  3830  sbcnestgfw  4369  sbcnestgf  4374  mpteq12f  5141  axrep2  5185  axnulALT  5200  dtru  5263  eusv1  5283  alxfr  5299  axprlem4  5318  axprlem5  5319  iota1  6326  dffv2  6750  fiint  8789  isf32lem9  9777  nd3  10005  axrepnd  10010  axpowndlem2  10014  axpowndlem3  10015  axacndlem4  10026  trclfvcotr  14363  relexpindlem  14416  fiinopn  21503  ex-natded9.26-2  28193  bnj1294  32084  bnj570  32172  bnj953  32206  bnj1204  32279  bnj1388  32300  frmin  33079  bj-ssbid2ALT  33991  bj-sb  34016  bj-spst  34018  bj-19.21bit  34019  bj-dtru  34134  bj-hbaeb2  34136  bj-hbnaeb  34138  bj-sbsb  34155  bj-nfcsym  34210  exlimim  34617  exellim  34619  difunieq  34649  wl-aleq  34769  wl-equsal1i  34777  wl-sb8t  34782  wl-2spsbbi  34795  wl-lem-exsb  34796  wl-lem-moexsb  34798  wl-mo2tf  34801  wl-eutf  34803  wl-mo2t  34805  wl-mo3t  34806  wl-sb8eut  34807  wl-ax11-lem2  34812  prtlem14  36004  axc5  36023  setindtr  39614  pm11.57  40714  pm11.59  40716  axc5c4c711toc7  40729  axc5c4c711to11  40730  axc11next  40731  eubiOLD  40761  ssralv2  40858  19.41rg  40877  hbexg  40883  ax6e2ndeq  40886  ssralv2VD  41193  19.41rgVD  41229  hbimpgVD  41231  hbexgVD  41233  ax6e2eqVD  41234  ax6e2ndeqVD  41236  vk15.4jVD  41241  ax6e2ndeqALT  41258  rexsb  43291  setrec1lem4  44787