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

Theorem sp 2056
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 2357.

This theorem shows that our obsolete axiom ax-c5 33615 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 2049. It is thought the best we can do using only Tarski's axioms is spw 1969. (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 1750 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2 19.8a 2054 . . 3 𝜑 → ∃𝑥 ¬ 𝜑)
32con1i 144 . 2 (¬ ∃𝑥 ¬ 𝜑𝜑)
41, 3sylbi 207 1 (∀𝑥𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1478  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-12 2049
This theorem depends on definitions:  df-bi 197  df-ex 1702
This theorem is referenced by:  spi  2057  sps  2058  2sp  2059  spsd  2060  19.21bi  2062  19.3  2072  19.9d  2073  axc4  2131  axc7  2133  axc7e  2134  axc16gb  2137  sb56  2152  19.12  2166  nfaldOLD  2168  nfrOLD  2192  19.3OLD  2206  ax12  2308  ax13ALT  2309  hbae  2319  ax12OLD  2345  ax12b  2349  sb2  2356  dfsb2  2377  sbequi  2379  nfsb4t  2393  exsb  2472  mo3  2511  mopick  2539  axi4  2597  axi5r  2598  nfcr  2759  rsp  2929  ceqex  3321  elrab3t  3350  abidnf  3362  mob2  3373  sbcnestgf  3972  mpteq12f  4696  axrep2  4738  axnulALT  4752  dtru  4822  eusv1  4825  alxfr  4843  iota1  5827  dffv2  6229  fiint  8182  isf32lem9  9128  nd3  9356  axrepnd  9361  axpowndlem2  9365  axpowndlem3  9366  axacndlem4  9377  trclfvcotr  13679  relexpindlem  13732  fiinopn  20626  ex-natded9.26-2  27125  bnj1294  30588  bnj570  30675  bnj953  30709  bnj1204  30780  bnj1388  30801  frmin  31428  bj-hbxfrbi  32223  bj-ssbft  32257  bj-ssbequ2  32258  bj-ssbid2ALT  32261  bj-sb  32292  bj-spst  32294  bj-19.21bit  32295  bj-19.3t  32304  bj-sb2v  32369  bj-axrep2  32405  bj-dtru  32413  bj-hbaeb2  32421  bj-hbnaeb  32423  bj-sbsb  32440  bj-nfcsym  32506  exlimim  32794  exellim  32797  wl-aleq  32930  wl-equsal1i  32937  wl-sb8t  32941  wl-lem-exsb  32956  wl-lem-moexsb  32958  wl-mo2tf  32961  wl-eutf  32963  wl-mo2t  32965  wl-mo3t  32966  wl-sb8eut  32967  wl-ax11-lem2  32971  nfbii2  33566  prtlem14  33606  axc5  33625  setindtr  37038  pm11.57  38038  pm11.59  38040  axc5c4c711toc7  38054  axc5c4c711to11  38055  axc11next  38056  iotain  38067  eubi  38086  ssralv2  38186  19.41rg  38215  hbexg  38221  ax6e2ndeq  38224  ssralv2VD  38552  19.41rgVD  38588  hbimpgVD  38590  hbexgVD  38592  ax6e2eqVD  38593  ax6e2ndeqVD  38595  vk15.4jVD  38600  ax6e2ndeqALT  38617  rexsb  40440  setrec1lem4  41685
  Copyright terms: Public domain W3C validator