Theorem sp 2176

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

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1539  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

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

This theorem is referenced by:  spi  2177  sps  2178  2sp  2179  spsd  2180  19.21bi  2182  19.3t  2194  19.3  2195  19.9d  2196  sb4av  2236  sbequ2  2241  axc16gb  2253  axc7  2310  axc4  2314  19.12  2320  exsb  2355  ax12  2422  ax12b  2423  ax13ALT  2424  hbae  2430  sb4a  2479  dfsb2  2492  nfsb4t  2498  mo3  2558  mopick  2621  axi4  2694  axi5r  2695  nfcrALT  2889  nfcriOLDOLD  2894  nfabdwOLD  2927  rsp  3244  ceqex  3639  elrab3t  3681  abidnf  3697  mob2  3710  sbcbi2OLD  3839  sbcnestgfw  4417  sbcnestgf  4422  ralidm  4510  mpteq12f  5235  axrep2  5287  axnulALT  5303  eusv1  5388  alxfr  5404  axprlem4  5423  axprlem5  5424  iota1  6517  dffv2  6983  fiint  9320  isf32lem9  10352  nd3  10580  axrepnd  10585  axpowndlem2  10589  axpowndlem3  10590  axacndlem4  10601  trclfvcotr  14952  relexpindlem  15006  fiinopn  22394  ex-natded9.26-2  29662  bnj1294  33816  bnj570  33904  bnj953  33938  bnj1204  34011  bnj1388  34032  bj-ssbid2ALT  35528  bj-sb  35553  bj-spst  35555  bj-19.21bit  35556  bj-substax12  35587  bj-hbaeb2  35684  bj-hbnaeb  35686  bj-sbsb  35703  bj-nfcsym  35767  exlimim  36211  exellim  36213  difunieq  36243  wl-aleq  36392  wl-equsal1i  36400  wl-sb8t  36405  wl-2spsbbi  36418  wl-lem-exsb  36419  wl-lem-moexsb  36421  wl-mo2tf  36424  wl-eutf  36426  wl-mo2t  36428  wl-mo3t  36429  wl-sb8eut  36430  wl-ax11-lem2  36436  mopickr  37220  prtlem14  37732  axc5  37751  setindtr  41748  unielss  41952  ismnushort  43045  pm11.57  43133  pm11.59  43135  axc5c4c711toc7  43148  axc5c4c711to11  43149  axc11next  43150  eubiOLD  43180  ssralv2  43277  19.41rg  43296  hbexg  43302  ax6e2ndeq  43305  ssralv2VD  43612  19.41rgVD  43648  hbimpgVD  43650  hbexgVD  43652  ax6e2eqVD  43653  ax6e2ndeqVD  43655  vk15.4jVD  43660  ax6e2ndeqALT  43677  rexsb  45793  ichnfimlem  46117  setrec1lem4  47688