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

Theorem sp 2051
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 2351.

This theorem shows that our obsolete axiom ax-c5 33987 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 2045. It is thought the best we can do using only Tarski's axioms is spw 1965. (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 1751 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2 19.8a 2050 . . 3 𝜑 → ∃𝑥 ¬ 𝜑)
32con1i 144 . 2 (¬ ∃𝑥 ¬ 𝜑𝜑)
41, 3sylbi 207 1 (∀𝑥𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1479  wex 1702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-12 2045
This theorem depends on definitions:  df-bi 197  df-ex 1703
This theorem is referenced by:  spi  2052  sps  2053  2sp  2054  spsd  2055  19.21bi  2057  19.3  2067  19.9d  2068  axc4  2128  axc7  2130  axc7e  2131  axc16gb  2134  sb56  2148  19.12  2162  nfaldOLD  2164  nfrOLD  2186  19.3OLD  2200  ax12  2302  ax13ALT  2303  hbae  2313  ax12OLD  2339  ax12b  2343  sb2  2350  dfsb2  2371  sbequi  2373  nfsb4t  2387  exsb  2466  mo3  2505  mopick  2533  axi4  2591  axi5r  2592  nfcr  2754  rsp  2926  ceqex  3327  elrab3t  3356  abidnf  3369  mob2  3380  sbcnestgf  3986  mpteq12f  4722  axrep2  4764  axnulALT  4778  dtru  4848  eusv1  4851  alxfr  4869  iota1  5853  dffv2  6258  fiint  8222  isf32lem9  9168  nd3  9396  axrepnd  9401  axpowndlem2  9405  axpowndlem3  9406  axacndlem4  9417  trclfvcotr  13731  relexpindlem  13784  fiinopn  20687  ex-natded9.26-2  27247  bnj1294  30862  bnj570  30949  bnj953  30983  bnj1204  31054  bnj1388  31075  frmin  31713  bj-hbxfrbi  32583  bj-ssbft  32617  bj-ssbequ2  32618  bj-ssbid2ALT  32621  bj-sb  32652  bj-spst  32654  bj-19.21bit  32655  bj-19.3t  32664  bj-sb2v  32728  bj-axrep2  32764  bj-dtru  32772  bj-hbaeb2  32780  bj-hbnaeb  32782  bj-sbsb  32799  bj-nfcsym  32861  exlimim  33160  exellim  33163  wl-aleq  33293  wl-equsal1i  33300  wl-sb8t  33304  wl-lem-exsb  33319  wl-lem-moexsb  33321  wl-mo2tf  33324  wl-eutf  33326  wl-mo2t  33328  wl-mo3t  33329  wl-sb8eut  33330  wl-ax11-lem2  33334  nfbii2  33938  prtlem14  33978  axc5  33997  setindtr  37410  pm11.57  38409  pm11.59  38411  axc5c4c711toc7  38425  axc5c4c711to11  38426  axc11next  38427  iotain  38438  eubi  38457  ssralv2  38557  19.41rg  38586  hbexg  38592  ax6e2ndeq  38595  ssralv2VD  38922  19.41rgVD  38958  hbimpgVD  38960  hbexgVD  38962  ax6e2eqVD  38963  ax6e2ndeqVD  38965  vk15.4jVD  38970  ax6e2ndeqALT  38987  rexsb  40931  setrec1lem4  42202
  Copyright terms: Public domain W3C validator