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

Theorem sp 2183
 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 2074. This theorem shows that our obsolete axiom ax-c5 36061 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 2178. It is thought the best we can do using only Tarski's axioms is spw 2042. Also see spvw 1986 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 1827 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2 19.8a 2181 . . 3 𝜑 → ∃𝑥 ¬ 𝜑)
32con1i 149 . 2 (¬ ∃𝑥 ¬ 𝜑𝜑)
41, 3sylbi 220 1 (∀𝑥𝜑𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1536  ∃wex 1781 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-12 2178 This theorem depends on definitions:  df-bi 210  df-ex 1782 This theorem is referenced by:  spi  2184  sps  2185  2sp  2186  spsd  2187  19.21bi  2189  19.3t  2202  19.3  2203  19.9d  2204  sb4av  2245  sbequ2  2251  sbequ2OLD  2252  axc16gb  2264  sb56OLD  2279  spsbimvOLD  2329  axc7  2337  axc4  2341  19.12  2347  exsb  2379  ax12  2446  ax12b  2447  ax13ALT  2448  hbae  2454  sb4a  2510  sb2vOLDOLD  2513  dfsb2  2533  sbequiOLD  2535  nfsb4t  2540  sb2vOLDALT  2584  sb2ALT  2588  dfsb2ALT  2592  sbequiALT  2597  nfsb4tALT  2605  mo3  2648  mopick  2710  axi4  2784  axi5r  2785  nfcr  2963  nfabdw  2995  rsp  3193  ceqex  3622  elrab3t  3656  abidnf  3671  mob2  3683  sbcbi2OLD  3808  sbcnestgfw  4343  sbcnestgf  4348  mpteq12f  5122  axrep2  5166  axnulALT  5181  dtru  5244  eusv1  5265  alxfr  5281  axprlem4  5300  axprlem5  5301  iota1  6305  dffv2  6729  fiint  8771  isf32lem9  9760  nd3  9988  axrepnd  9993  axpowndlem2  9997  axpowndlem3  9998  axacndlem4  10009  trclfvcotr  14348  relexpindlem  14401  fiinopn  21485  ex-natded9.26-2  28184  bnj1294  32097  bnj570  32185  bnj953  32219  bnj1204  32292  bnj1388  32313  frmin  33092  bj-ssbid2ALT  34004  bj-sb  34029  bj-spst  34031  bj-19.21bit  34032  bj-subst  34063  bj-dtru  34148  bj-hbaeb2  34150  bj-hbnaeb  34152  bj-sbsb  34169  bj-nfcsym  34233  exlimim  34643  exellim  34645  difunieq  34675  wl-aleq  34822  wl-equsal1i  34830  wl-sb8t  34835  wl-2spsbbi  34848  wl-lem-exsb  34849  wl-lem-moexsb  34851  wl-mo2tf  34854  wl-eutf  34856  wl-mo2t  34858  wl-mo3t  34859  wl-sb8eut  34860  wl-ax11-lem2  34865  prtlem14  36052  axc5  36071  setindtr  39772  pm11.57  40904  pm11.59  40906  axc5c4c711toc7  40919  axc5c4c711to11  40920  axc11next  40921  eubiOLD  40951  ssralv2  41048  19.41rg  41067  hbexg  41073  ax6e2ndeq  41076  ssralv2VD  41383  19.41rgVD  41419  hbimpgVD  41421  hbexgVD  41423  ax6e2eqVD  41424  ax6e2ndeqVD  41426  vk15.4jVD  41431  ax6e2ndeqALT  41448  rexsb  43473  ichnfimlem  43799  setrec1lem4  45027
 Copyright terms: Public domain W3C validator