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

Theorem sp 1763
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 2087.

This theorem shows that our obsolete axiom ax-4 2211 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 1761. It is thought the best we can do using only Tarski's axioms is spw 1706. (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 1581 . 2  |-  ( A. x ph  <->  -.  E. x  -.  ph )
2 19.8a 1762 . . 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 1549   E.wex 1550
This theorem is referenced by:  ax5o  1765  ax6o  1766  spi  1769  sps  1770  spsd  1771  19.8aOLD  1772  19.21bi  1774  nfr  1777  19.3  1791  hbnOLD  1802  hba1OLD  1805  hbimdOLD  1835  spimehOLD  1840  equsalhwOLD  1861  19.21hOLD  1862  19.12  1869  19.12OLD  1870  nfald  1871  cbv3hvOLD  1879  19.21tOLD  1886  19.38OLD  1895  spimtOLD  1956  cbv1h  1974  ax12olem3OLD  2013  ax12  2019  ax12OLD  2020  dvelimvOLD  2028  ax9OLD  2033  hbae  2040  hbaeOLD  2041  ax11b  2078  equveliOLD  2082  sb2  2086  dfsb2  2115  a16gb  2134  nfsb4t  2154  nfsb4tOLD  2155  sb56  2173  sb6  2174  sbal1  2202  exsb  2206  ax4  2221  mo  2302  mopick  2342  2eu1  2360  axi4  2407  axi5r  2408  nfcr  2563  rsp  2758  ceqex  3058  abidnf  3095  mob2  3106  csbie2t  3287  sbcnestgf  3290  mpteq12f  4277  axrep2  4314  axnulALT  4328  dtru  4382  copsex2t  4435  ssopab2  4472  eusv1  4709  alxfr  4728  iota1  5424  dffv2  5788  fiint  7375  isf32lem9  8233  nd3  8456  axrepnd  8461  axpowndlem2  8465  axacndlem4  8477  fiinopn  16966  ex-natded9.26-2  21720  relexpindlem  25131  fundmpss  25382  frmin  25509  wfrlem5  25534  frrlem5  25578  wl-aleq  26227  mbfresfi  26243  prtlem14  26714  setindtr  27086  pm11.57  27556  pm11.59  27558  ax4567to6  27572  ax4567to7  27573  ax10ext  27574  iotain  27585  pm14.123b  27594  eubi  27604  rexsb  27913  ssralv2  28552  19.41rg  28574  hbexg  28580  a9e2ndeq  28583  ssralv2VD  28915  19.41rgVD  28951  hbimpgVD  28953  hbexgVD  28955  a9e2eqVD  28956  a9e2ndeqVD  28958  vk15.4jVD  28963  a9e2ndeqALT  28980  bnj1294  29126  bnj570  29213  bnj953  29247  bnj1204  29318  bnj1388  29339  19.12vAUX7  29391  ax12olem3aAUX7  29394  dvelimvNEW7  29399  ax9NEW7  29405  hbaewAUX7  29415  spimtNEW7  29444  equveliNEW7  29465  sb2NEW7  29474  a16gbNEW7  29484  nfsb4twAUX7  29513  sb56NEW7  29533  sb6NEW7  29534  exsbNEW7  29536  sbal1NEW7  29552  ax11bNEW7  29559  dfsb2NEW7  29575  ax7w1AUX7  29582  hbaew0AUX7  29584  ax7w7AUX7  29590  ax7w4AUX7  29595  ax7w10AUX7  29599  ax7w11AUX7  29600  ax7w18AUX7  29614  19.12OLD7  29623  hbaeOLD7  29645  nfsb4tOLD7  29682  nfsb4tw2AUXOLD7  29683
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator