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 37753 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 1540  ∃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  axc16gb  2254  axc7  2311  axc4  2315  19.12  2321  exsb  2356  ax12  2423  ax12b  2424  ax13ALT  2425  hbae  2431  sb4a  2480  dfsb2  2493  nfsb4t  2499  mo3  2559  mopick  2622  axi4  2695  axi5r  2696  nfcrALT  2890  nfcriOLDOLD  2895  nfabdwOLD  2928  rsp  3245  ceqex  3641  elrab3t  3683  abidnf  3699  mob2  3712  sbcbi2OLD  3841  sbcnestgfw  4419  sbcnestgf  4424  ralidm  4512  mpteq12f  5237  axrep2  5289  axnulALT  5305  eusv1  5390  alxfr  5406  axprlem4  5425  axprlem5  5426  iota1  6521  dffv2  6987  fiint  9324  isf32lem9  10356  nd3  10584  axrepnd  10589  axpowndlem2  10593  axpowndlem3  10594  axacndlem4  10605  trclfvcotr  14956  relexpindlem  15010  fiinopn  22403  ex-natded9.26-2  29673  bnj1294  33828  bnj570  33916  bnj953  33950  bnj1204  34023  bnj1388  34044  bj-ssbid2ALT  35540  bj-sb  35565  bj-spst  35567  bj-19.21bit  35568  bj-substax12  35599  bj-hbaeb2  35696  bj-hbnaeb  35698  bj-sbsb  35715  bj-nfcsym  35779  exlimim  36223  exellim  36225  difunieq  36255  wl-aleq  36404  wl-equsal1i  36412  wl-sb8t  36417  wl-2spsbbi  36430  wl-lem-exsb  36431  wl-lem-moexsb  36433  wl-mo2tf  36436  wl-eutf  36438  wl-mo2t  36440  wl-mo3t  36441  wl-sb8eut  36442  wl-ax11-lem2  36448  mopickr  37232  prtlem14  37744  axc5  37763  setindtr  41763  unielss  41967  ismnushort  43060  pm11.57  43148  pm11.59  43150  axc5c4c711toc7  43163  axc5c4c711to11  43164  axc11next  43165  eubiOLD  43195  ssralv2  43292  19.41rg  43311  hbexg  43317  ax6e2ndeq  43320  ssralv2VD  43627  19.41rgVD  43663  hbimpgVD  43665  hbexgVD  43667  ax6e2eqVD  43668  ax6e2ndeqVD  43670  vk15.4jVD  43675  ax6e2ndeqALT  43692  rexsb  45807  ichnfimlem  46131  setrec1lem4  47735