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

Theorem sp 1990
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 2245.

This theorem shows that our obsolete axiom ax-c5 33080 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 1983. It is thought the best we can do using only Tarski's axioms is spw 1916. (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 1731 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2 19.8a 1988 . . 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 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-12 1983
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  axc4  1991  axc7  1992  spi  1995  sps  1996  2sp  1997  spsd  1998  19.21bi  2000  nfr  2004  19.3  2018  axc16gb  2073  19.12  2082  nfald  2083  sb56  2128  ax12  2196  ax13OLD  2197  hbae  2207  ax12OLD  2233  ax12b  2237  sb2  2244  dfsb2  2265  sbequi  2267  nfsb4t  2281  exsb  2360  mo3  2399  mopick  2427  axi4  2485  axi5r  2486  nfcr  2647  rsp  2817  ceqex  3207  elrab3t  3234  abidnf  3246  mob2  3257  sbcnestgf  3850  mpteq12f  4559  axrep2  4599  axnulALT  4613  dtru  4682  eusv1  4685  alxfr  4703  iota1  5672  dffv2  6070  fiint  8002  isf32lem9  8946  nd3  9170  axrepnd  9175  axpowndlem2  9179  axpowndlem3  9180  axacndlem4  9191  trclfvcotr  13461  relexpindlem  13514  fiinopn  20438  ex-natded9.26-2  26411  bnj1294  29991  bnj570  30078  bnj953  30112  bnj1204  30183  bnj1388  30204  frmin  30829  bj-hbxfrbi  31630  bj-ssbft  31669  bj-ssbequ2  31670  bj-ssbid2ALT  31673  bj-sb  31702  bj-spst  31704  bj-19.21bit  31705  bj-19.3t  31714  bj-sb2v  31782  bj-axrep2  31822  bj-dtru  31830  bj-hbaeb2  31838  bj-hbnaeb  31840  bj-sbsb  31857  bj-nfcsym  31914  bj-ax9  31918  exlimim  32200  exellim  32203  wl-19.9d  32343  wl-aleq  32394  wl-equsal1i  32402  wl-sb8t  32406  wl-lem-exsb  32421  wl-lem-moexsb  32423  wl-mo2tf  32426  wl-eutf  32428  wl-mo2t  32430  wl-mo3t  32431  wl-sb8eut  32432  wl-ax11-lem2  32436  nfbii2  33031  prtlem14  33071  axc5  33090  setindtr  36503  pm11.57  37512  pm11.59  37514  axc5c4c711toc7  37528  axc5c4c711to11  37529  axc11next  37530  iotain  37541  eubi  37560  ssralv2  37659  19.41rg  37688  hbexg  37694  ax6e2ndeq  37697  ssralv2VD  38025  19.41rgVD  38061  hbimpgVD  38063  hbexgVD  38065  ax6e2eqVD  38066  ax6e2ndeqVD  38068  vk15.4jVD  38073  ax6e2ndeqALT  38090  rexsb  39728
  Copyright terms: Public domain W3C validator