Theorem sp 2207

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

This theorem shows that our obsolete axiom ax-c5 34692 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 2203. It is thought the best we can do using only Tarski's axioms is spw 2123. (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 1901	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		19.8a 2206	. . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
3	2	con1i 146	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑)
4	1, 3	sylbi 207	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1629  ∃wex 1852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-12 2203

This theorem depends on definitions:  df-bi 197  df-ex 1853

This theorem is referenced by:  spi  2208  sps  2209  2sp  2210  spsd  2211  19.21bi  2213  19.3  2224  19.9d  2225  19.9dOLDOLD  2226  sb56  2271  sb6  2272  axc4  2294  axc7  2296  axc7eOLD  2298  axc16gb  2301  19.12  2326  nfaldOLD  2328  nfrOLD  2350  19.3OLD  2364  ax12  2460  ax13ALT  2461  hbae  2467  ax12b  2491  sb2  2498  dfsb2  2520  sbequi  2522  nfsb4t  2536  exsb  2616  mo3  2656  mopick  2684  axi4  2742  axi5r  2743  nfcr  2905  rsp  3078  ceqex  3484  elrab3t  3515  abidnf  3528  mob2  3539  sbcnestgf  4140  mpteq12f  4866  axrep2  4908  axnulALT  4922  dtru  4989  eusv1  4992  alxfr  5008  iota1  6009  dffv2  6414  fiint  8394  isf32lem9  9386  nd3  9614  axrepnd  9619  axpowndlem2  9623  axpowndlem3  9624  axacndlem4  9635  trclfvcotr  13959  relexpindlem  14012  fiinopn  20927  ex-natded9.26-2  27620  bnj1294  31227  bnj570  31314  bnj953  31348  bnj1204  31419  bnj1388  31440  frmin  32080  bj-hbxfrbi  32946  bj-ssbft  32980  bj-ssbequ2  32981  bj-ssbid2ALT  32984  bj-sb  33015  bj-spst  33017  bj-19.21bit  33018  bj-19.3t  33027  bj-sb2v  33090  bj-axrep2  33126  bj-dtru  33134  bj-hbaeb2  33141  bj-hbnaeb  33143  bj-sbsb  33160  bj-nfcsym  33216  exlimim  33527  exellim  33530  wl-aleq  33658  wl-equsal1i  33665  wl-sb8t  33669  wl-lem-exsb  33683  wl-lem-moexsb  33685  wl-mo2tf  33688  wl-eutf  33690  wl-mo2t  33692  wl-mo3t  33693  wl-sb8eut  33694  wl-ax11-lem2  33698  nfbii2  34300  prtlem14  34683  axc5  34702  setindtr  38118  pm11.57  39116  pm11.59  39118  axc5c4c711toc7  39132  axc5c4c711to11  39133  axc11next  39134  iotain  39145  eubi  39164  ssralv2  39263  19.41rg  39292  hbexg  39298  ax6e2ndeq  39301  ssralv2VD  39625  19.41rgVD  39661  hbimpgVD  39663  hbexgVD  39665  ax6e2eqVD  39666  ax6e2ndeqVD  39668  vk15.4jVD  39673  ax6e2ndeqALT  39690  rexsb  41689  setrec1lem4  42966