Theorem sp 2183

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

This theorem shows that our obsolete axiom ax-c5 38884 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 2177. It is thought the best we can do using only Tarski's axioms is spw 2033. Also see spvw 1980 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 2181	. . 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 2007  ax-12 2177

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

This theorem is referenced by:  spi  2184  sps  2185  2sp  2186  spsd  2187  19.21bi  2189  19.3t  2201  19.3  2202  19.9d  2203  sb4av  2244  sbequ2  2249  axc16gb  2262  axc7  2317  axc4  2321  19.12  2327  exsb  2362  ax12  2428  ax12b  2429  ax13ALT  2430  hbae  2436  sb4a  2485  dfsb2  2498  nfsb4t  2504  mo3  2564  mopick  2625  axi4  2699  axi5r  2700  nfcrALT  2896  rsp  3247  ceqex  3652  elrab3t  3691  abidnf  3708  mob2  3721  sbcnestgfw  4421  sbcnestgf  4426  ralidm  4512  mpteq12f  5230  axrep2  5282  axnulALT  5304  eusv1  5391  alxfr  5407  axprlem4OLD  5429  axprlem5OLD  5430  iota1  6538  dffv2  7004  fiint  9366  fiintOLD  9367  isf32lem9  10401  nd3  10629  axrepnd  10634  axpowndlem2  10638  axpowndlem3  10639  axacndlem4  10650  trclfvcotr  15048  relexpindlem  15102  fiinopn  22907  ex-natded9.26-2  30439  bnj1294  34831  bnj570  34919  bnj953  34953  bnj1204  35026  bnj1388  35047  in-ax8  36225  ss-ax8  36226  bj-ssbid2ALT  36664  bj-sb  36688  bj-spst  36690  bj-19.21bit  36691  bj-substax12  36722  bj-hbaeb2  36819  bj-hbnaeb  36821  bj-sbsb  36838  bj-nfcsym  36900  exlimim  37343  exellim  37345  difunieq  37375  wl-aleq  37536  wl-equsal1i  37545  wl-sb8t  37553  wl-2spsbbi  37566  wl-lem-exsb  37567  wl-lem-moexsb  37569  wl-mo2tf  37572  wl-eutf  37574  wl-mo2t  37576  wl-mo3t  37577  wl-sb8eut  37579  wl-ax11-lem2  37587  mopickr  38364  prtlem14  38875  axc5  38894  setindtr  43036  unielss  43230  ismnushort  44320  pm11.57  44408  pm11.59  44410  axc5c4c711toc7  44423  axc5c4c711to11  44424  axc11next  44425  eubiOLD  44455  ssralv2  44551  19.41rg  44570  hbexg  44576  ax6e2ndeq  44579  ssralv2VD  44886  19.41rgVD  44922  hbimpgVD  44924  hbexgVD  44926  ax6e2eqVD  44927  ax6e2ndeqVD  44929  vk15.4jVD  44934  ax6e2ndeqALT  44951  rexsb  47111  ichnfimlem  47450  setrec1lem4  49209