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

Theorem sp 2039
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 2340.

This theorem shows that our obsolete axiom ax-c5 32989 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 2032. It is thought the best we can do using only Tarski's axioms is spw 1953. (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 1742 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2 19.8a 2037 . . 3 𝜑 → ∃𝑥 ¬ 𝜑)
32con1i 142 . 2 (¬ ∃𝑥 ¬ 𝜑𝜑)
41, 3sylbi 205 1 (∀𝑥𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1472  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2032
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  spi  2040  sps  2041  2sp  2042  spsd  2043  19.21bi  2045  19.3  2055  19.9d  2056  axc4  2113  axc7  2115  axc7e  2116  axc16gb  2119  sb56  2134  19.12  2148  nfaldOLD  2150  nfrOLD  2174  19.3OLD  2188  ax12  2291  ax13OLD  2292  hbae  2302  ax12OLD  2328  ax12b  2332  sb2  2339  dfsb2  2360  sbequi  2362  nfsb4t  2376  exsb  2455  mo3  2494  mopick  2522  axi4  2580  axi5r  2581  nfcr  2742  rsp  2912  ceqex  3302  elrab3t  3329  abidnf  3341  mob2  3352  sbcnestgf  3946  mpteq12f  4655  axrep2  4695  axnulALT  4709  dtru  4778  eusv1  4781  alxfr  4799  iota1  5768  dffv2  6166  fiint  8099  isf32lem9  9043  nd3  9267  axrepnd  9272  axpowndlem2  9276  axpowndlem3  9277  axacndlem4  9288  trclfvcotr  13544  relexpindlem  13597  fiinopn  20473  ex-natded9.26-2  26435  bnj1294  29948  bnj570  30035  bnj953  30069  bnj1204  30140  bnj1388  30161  frmin  30789  bj-hbxfrbi  31598  bj-ssbft  31637  bj-ssbequ2  31638  bj-ssbid2ALT  31641  bj-sb  31670  bj-spst  31672  bj-19.21bit  31673  bj-19.3t  31682  bj-sb2v  31750  bj-axrep2  31790  bj-dtru  31798  bj-hbaeb2  31806  bj-hbnaeb  31808  bj-sbsb  31825  bj-nfcsym  31882  bj-ax9  31886  exlimim  32168  exellim  32171  wl-aleq  32304  wl-equsal1i  32311  wl-sb8t  32315  wl-lem-exsb  32330  wl-lem-moexsb  32332  wl-mo2tf  32335  wl-eutf  32337  wl-mo2t  32339  wl-mo3t  32340  wl-sb8eut  32341  wl-ax11-lem2  32345  nfbii2  32940  prtlem14  32980  axc5  32999  setindtr  36412  pm11.57  37414  pm11.59  37416  axc5c4c711toc7  37430  axc5c4c711to11  37431  axc11next  37432  iotain  37443  eubi  37462  ssralv2  37561  19.41rg  37590  hbexg  37596  ax6e2ndeq  37599  ssralv2VD  37927  19.41rgVD  37963  hbimpgVD  37965  hbexgVD  37967  ax6e2eqVD  37968  ax6e2ndeqVD  37970  vk15.4jVD  37975  ax6e2ndeqALT  37992  rexsb  39621
  Copyright terms: Public domain W3C validator