Theorem sp 2180

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

This theorem shows that our obsolete axiom ax-c5 38864 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 2174. It is thought the best we can do using only Tarski's axioms is spw 2030. Also see spvw 1977 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 2178	. . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
3	2	con1i 147	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑)
4	1, 3	sylbi 217	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1534  ∃wex 1775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-12 2174

This theorem depends on definitions:  df-bi 207  df-ex 1776

This theorem is referenced by:  spi  2181  sps  2182  2sp  2183  spsd  2184  19.21bi  2186  19.3t  2198  19.3  2199  19.9d  2200  sb4av  2241  sbequ2  2246  axc16gb  2259  axc7  2315  axc4  2319  19.12  2325  exsb  2359  ax12  2425  ax12b  2426  ax13ALT  2427  hbae  2433  sb4a  2482  dfsb2  2495  nfsb4t  2501  mo3  2561  mopick  2622  axi4  2696  axi5r  2697  nfcrALT  2893  rsp  3244  ceqex  3651  elrab3t  3693  abidnf  3710  mob2  3723  sbcnestgfw  4426  sbcnestgf  4431  ralidm  4517  mpteq12f  5235  axrep2  5287  axnulALT  5309  eusv1  5396  alxfr  5412  axprlem4OLD  5434  axprlem5OLD  5435  iota1  6539  dffv2  7003  fiint  9363  fiintOLD  9364  isf32lem9  10398  nd3  10626  axrepnd  10631  axpowndlem2  10635  axpowndlem3  10636  axacndlem4  10647  trclfvcotr  15044  relexpindlem  15098  fiinopn  22922  ex-natded9.26-2  30448  bnj1294  34809  bnj570  34897  bnj953  34931  bnj1204  35004  bnj1388  35025  in-ax8  36206  ss-ax8  36207  bj-ssbid2ALT  36645  bj-sb  36669  bj-spst  36671  bj-19.21bit  36672  bj-substax12  36703  bj-hbaeb2  36800  bj-hbnaeb  36802  bj-sbsb  36819  bj-nfcsym  36881  exlimim  37324  exellim  37326  difunieq  37356  wl-aleq  37515  wl-equsal1i  37524  wl-sb8t  37532  wl-2spsbbi  37545  wl-lem-exsb  37546  wl-lem-moexsb  37548  wl-mo2tf  37551  wl-eutf  37553  wl-mo2t  37555  wl-mo3t  37556  wl-sb8eut  37558  wl-ax11-lem2  37566  mopickr  38344  prtlem14  38855  axc5  38874  setindtr  43012  unielss  43206  ismnushort  44296  pm11.57  44384  pm11.59  44386  axc5c4c711toc7  44399  axc5c4c711to11  44400  axc11next  44401  eubiOLD  44431  ssralv2  44528  19.41rg  44547  hbexg  44553  ax6e2ndeq  44556  ssralv2VD  44863  19.41rgVD  44899  hbimpgVD  44901  hbexgVD  44903  ax6e2eqVD  44904  ax6e2ndeqVD  44906  vk15.4jVD  44911  ax6e2ndeqALT  44928  rexsb  47048  ichnfimlem  47387  setrec1lem4  48920