MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sp Structured version   Visualization version   GIF version

Theorem sp 2172
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 2064.

This theorem shows that our obsolete axiom ax-c5 35899 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 2167. It is thought the best we can do using only Tarski's axioms is spw 2032. Also see spvw 1976 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
StepHypRef Expression
1 alex 1817 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2 19.8a 2170 . . 3 𝜑 → ∃𝑥 ¬ 𝜑)
32con1i 149 . 2 (¬ ∃𝑥 ¬ 𝜑𝜑)
41, 3sylbi 218 1 (∀𝑥𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1526  wex 1771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-ex 1772
This theorem is referenced by:  spi  2173  sps  2174  2sp  2175  spsd  2176  19.21bi  2178  19.3t  2191  19.3  2192  19.9d  2193  sb4av  2234  sbequ2  2240  sbequ2OLD  2241  axc16gb  2253  sb56OLD  2269  spsbimvOLD  2319  axc7  2327  axc4  2331  19.12  2337  exsb  2369  ax12  2437  ax12b  2438  ax13ALT  2439  hbae  2445  sb4a  2502  sb2vOLDOLD  2505  dfsb2  2525  sbequiOLD  2527  nfsb4t  2532  sb2vOLDALT  2576  sb2ALT  2580  dfsb2ALT  2584  sbequiALT  2589  nfsb4tALT  2597  mo3  2641  mopick  2703  axi4  2779  axi5r  2780  nfcr  2963  nfabdw  2997  rsp  3202  ralcom2w  3360  ceqex  3642  elrab3t  3676  abidnf  3691  mob2  3703  sbcbi2  3828  sbcnestgfw  4367  sbcnestgf  4372  mpteq12f  5140  axrep2  5184  axnulALT  5199  dtru  5262  eusv1  5282  alxfr  5298  axprlem4  5317  axprlem5  5318  iota1  6325  dffv2  6749  fiint  8783  isf32lem9  9771  nd3  9999  axrepnd  10004  axpowndlem2  10008  axpowndlem3  10009  axacndlem4  10020  trclfvcotr  14357  relexpindlem  14410  fiinopn  21437  ex-natded9.26-2  28126  bnj1294  31988  bnj570  32076  bnj953  32110  bnj1204  32181  bnj1388  32202  frmin  32981  bj-ssbid2ALT  33893  bj-sb  33918  bj-spst  33920  bj-19.21bit  33921  bj-dtru  34036  bj-hbaeb2  34038  bj-hbnaeb  34040  bj-sbsb  34057  bj-nfcsym  34112  exlimim  34505  exellim  34507  difunieq  34537  wl-aleq  34656  wl-equsal1i  34664  wl-sb8t  34669  wl-2spsbbi  34682  wl-lem-exsb  34683  wl-lem-moexsb  34685  wl-mo2tf  34688  wl-eutf  34690  wl-mo2t  34692  wl-mo3t  34693  wl-sb8eut  34694  wl-ax11-lem2  34699  prtlem14  35890  axc5  35909  setindtr  39499  pm11.57  40598  pm11.59  40600  axc5c4c711toc7  40613  axc5c4c711to11  40614  axc11next  40615  eubiOLD  40645  ssralv2  40742  19.41rg  40761  hbexg  40767  ax6e2ndeq  40770  ssralv2VD  41077  19.41rgVD  41113  hbimpgVD  41115  hbexgVD  41117  ax6e2eqVD  41118  ax6e2ndeqVD  41120  vk15.4jVD  41125  ax6e2ndeqALT  41142  rexsb  43174  setrec1lem4  44721
  Copyright terms: Public domain W3C validator