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

Theorem sp 1755
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).

For the axiom of specialization presented in many logic textbooks, see theorem stdpc4 2058.

This theorem shows that our obsolete axiom ax-4 2170 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 auxilliary axiom scheme ax-11 1753. It is thought the best we can do using only Tarski's axioms is spw 1701. (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  |-  ( A. x ph  ->  ph )

Proof of Theorem sp
StepHypRef Expression
1 alex 1578 . 2  |-  ( A. x ph  <->  -.  E. x  -.  ph )
2 19.8a 1754 . . 3  |-  ( -. 
ph  ->  E. x  -.  ph )
32con1i 123 . 2  |-  ( -. 
E. x  -.  ph  ->  ph )
41, 3sylbi 188 1  |-  ( A. x ph  ->  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1546   E.wex 1547
This theorem is referenced by:  ax5o  1757  ax6o  1758  spi  1761  sps  1762  spsd  1763  19.8aOLD  1764  19.21bi  1766  nfr  1769  hbnOLD  1785  19.3  1793  hba1OLD  1795  hbimdOLD  1825  spimehOLD  1830  equsalhwOLD  1851  19.21hOLD  1852  19.12  1859  19.12OLD  1860  cbv3hvOLD  1863  nfald  1864  19.21tOLD  1875  19.38OLD  1884  spimtOLD  1947  ax12olem3OLD  1969  ax12  1975  ax12OLD  1976  dvelimvOLD  1987  ax9OLD  1991  hbae  1999  equveli  2025  ax11b  2031  sb2  2057  a16gb  2084  dfsb2  2089  nfsb4t  2114  sb56  2132  sb6  2133  sbal1  2161  exsb  2165  ax4  2180  mo  2261  mopick  2301  2eu1  2319  axi4  2360  axi5r  2361  nfcr  2516  rsp  2710  ceqex  3010  abidnf  3047  mob2  3058  csbie2t  3239  sbcnestgf  3242  mpteq12f  4227  axrep2  4264  axnulALT  4278  dtru  4332  copsex2t  4385  ssopab2  4422  eusv1  4658  alxfr  4677  iota1  5373  dffv2  5736  fiint  7320  isf32lem9  8175  nd3  8398  axrepnd  8403  axpowndlem2  8407  axacndlem4  8419  fiinopn  16898  ex-natded9.26-2  21577  relexpindlem  24919  fundmpss  25147  frmin  25267  wfrlem5  25285  frrlem5  25310  prtlem14  26415  setindtr  26787  pm11.57  27258  pm11.59  27260  ax4567to6  27274  ax4567to7  27275  ax10ext  27276  iotain  27287  pm14.123b  27296  eubi  27306  rexsb  27615  ssralv2  27959  19.41rg  27981  hbexg  27987  a9e2ndeq  27990  ssralv2VD  28320  19.41rgVD  28356  hbimpgVD  28358  hbexgVD  28360  a9e2eqVD  28361  a9e2ndeqVD  28363  vk15.4jVD  28368  a9e2ndeqALT  28386  bnj1294  28528  bnj570  28615  bnj953  28649  bnj1204  28720  bnj1388  28741  19.12vAUX7  28793  ax12olem3aAUX7  28796  dvelimvNEW7  28801  ax9NEW7  28807  hbaewAUX7  28817  spimtNEW7  28846  equveliNEW7  28865  sb2NEW7  28874  a16gbNEW7  28884  nfsb4twAUX7  28913  sb56NEW7  28930  sb6NEW7  28931  exsbNEW7  28933  sbal1NEW7  28949  ax11bNEW7  28956  dfsb2NEW7  28972  ax7w1AUX7  28978  hbaew0AUX7  28980  ax7w7AUX7  28986  ax7w4AUX7  28991  19.12OLD7  29003  hbaeOLD7  29025  nfsb4tOLD7  29062  nfsb4tw2AUXOLD7  29063
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator