Theorem sp 2184

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 38876 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 2178. It is thought the best we can do using only Tarski's axioms is spw 2034. 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 1826	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		19.8a 2182	. . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
3	2	con1i 147	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑)
4	1, 3	sylbi 217	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1538  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

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

This theorem is referenced by:  spi  2185  sps  2186  2sp  2187  spsd  2188  19.21bi  2190  19.3t  2202  19.3  2203  19.9d  2204  sb4av  2245  sbequ2  2250  axc16gb  2263  axc7  2316  axc4  2320  19.12  2326  exsb  2357  ax12  2421  ax12b  2422  ax13ALT  2423  hbae  2429  sb4a  2478  dfsb2  2491  nfsb4t  2497  mo3  2557  mopick  2618  axi4  2692  axi5r  2693  nfcrALT  2882  rsp  3225  ceqex  3618  elrab3t  3658  abidnf  3673  mob2  3686  sbcnestgfw  4384  sbcnestgf  4389  ralidm  4475  mpteq12f  5192  axrep2  5237  axnulALT  5259  eusv1  5346  alxfr  5362  axprlem4OLD  5384  axprlem5OLD  5385  iota1  6488  dffv2  6956  fiint  9277  fiintOLD  9278  isf32lem9  10314  nd3  10542  axrepnd  10547  axpowndlem2  10551  axpowndlem3  10552  axacndlem4  10563  trclfvcotr  14975  relexpindlem  15029  fiinopn  22788  ex-natded9.26-2  30349  bnj1294  34807  bnj570  34895  bnj953  34929  bnj1204  35002  bnj1388  35023  in-ax8  36212  ss-ax8  36213  bj-ssbid2ALT  36651  bj-sb  36675  bj-spst  36677  bj-19.21bit  36678  bj-substax12  36709  bj-hbaeb2  36806  bj-hbnaeb  36808  bj-sbsb  36825  bj-nfcsym  36887  exlimim  37330  exellim  37332  difunieq  37362  wl-aleq  37523  wl-equsal1i  37532  wl-sb8t  37540  wl-2spsbbi  37553  wl-lem-exsb  37554  wl-lem-moexsb  37556  wl-mo2tf  37559  wl-eutf  37561  wl-mo2t  37563  wl-mo3t  37564  wl-sb8eut  37566  wl-ax11-lem2  37574  mopickr  38345  prtlem14  38867  axc5  38886  setindtr  43013  unielss  43207  ismnushort  44290  pm11.57  44378  pm11.59  44380  axc5c4c711toc7  44393  axc5c4c711to11  44394  axc11next  44395  eubiOLD  44425  ssralv2  44521  19.41rg  44540  hbexg  44546  ax6e2ndeq  44549  ssralv2VD  44855  19.41rgVD  44891  hbimpgVD  44893  hbexgVD  44895  ax6e2eqVD  44896  ax6e2ndeqVD  44898  vk15.4jVD  44903  ax6e2ndeqALT  44920  rexsb  47100  ichnfimlem  47464  setrec1lem4  49679