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 37845 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  3640  elrab3t  3682  abidnf  3698  mob2  3711  sbcbi2OLD  3840  sbcnestgfw  4418  sbcnestgf  4423  ralidm  4511  mpteq12f  5236  axrep2  5288  axnulALT  5304  eusv1  5389  alxfr  5405  axprlem4  5424  axprlem5  5425  iota1  6520  dffv2  6986  fiint  9326  isf32lem9  10358  nd3  10586  axrepnd  10591  axpowndlem2  10595  axpowndlem3  10596  axacndlem4  10607  trclfvcotr  14958  relexpindlem  15012  fiinopn  22410  ex-natded9.26-2  29711  bnj1294  33897  bnj570  33985  bnj953  34019  bnj1204  34092  bnj1388  34113  bj-ssbid2ALT  35632  bj-sb  35657  bj-spst  35659  bj-19.21bit  35660  bj-substax12  35691  bj-hbaeb2  35788  bj-hbnaeb  35790  bj-sbsb  35807  bj-nfcsym  35871  exlimim  36315  exellim  36317  difunieq  36347  wl-aleq  36496  wl-equsal1i  36504  wl-sb8t  36509  wl-2spsbbi  36522  wl-lem-exsb  36523  wl-lem-moexsb  36525  wl-mo2tf  36528  wl-eutf  36530  wl-mo2t  36532  wl-mo3t  36533  wl-sb8eut  36534  wl-ax11-lem2  36540  mopickr  37324  prtlem14  37836  axc5  37855  setindtr  41851  unielss  42055  ismnushort  43148  pm11.57  43236  pm11.59  43238  axc5c4c711toc7  43251  axc5c4c711to11  43252  axc11next  43253  eubiOLD  43283  ssralv2  43380  19.41rg  43399  hbexg  43405  ax6e2ndeq  43408  ssralv2VD  43715  19.41rgVD  43751  hbimpgVD  43753  hbexgVD  43755  ax6e2eqVD  43756  ax6e2ndeqVD  43758  vk15.4jVD  43763  ax6e2ndeqALT  43780  rexsb  45892  ichnfimlem  46216  setrec1lem4  47819