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  26704  setindtr  27076  pm11.57  27546  pm11.59  27548  ax4567to6  27562  ax4567to7  27563  ax10ext  27564  iotain  27575  pm14.123b  27584  eubi  27594  rexsb  27903  ssralv2  28542  19.41rg  28564  hbexg  28570  a9e2ndeq  28573  ssralv2VD  28905  19.41rgVD  28941  hbimpgVD  28943  hbexgVD  28945  a9e2eqVD  28946  a9e2ndeqVD  28948  vk15.4jVD  28953  a9e2ndeqALT  28970  bnj1294  29116  bnj570  29203  bnj953  29237  bnj1204  29308  bnj1388  29329  19.12vAUX7  29381  ax12olem3aAUX7  29384  dvelimvNEW7  29389  ax9NEW7  29395  hbaewAUX7  29405  spimtNEW7  29434  equveliNEW7  29455  sb2NEW7  29464  a16gbNEW7  29474  nfsb4twAUX7  29503  sb56NEW7  29523  sb6NEW7  29524  exsbNEW7  29526  sbal1NEW7  29542  ax11bNEW7  29549  dfsb2NEW7  29565  ax7w1AUX7  29572  hbaew0AUX7  29574  ax7w7AUX7  29580  ax7w4AUX7  29585  ax7w10AUX7  29589  ax7w11AUX7  29590  ax7w18AUX7  29604  19.12OLD7  29613  hbaeOLD7  29635  nfsb4tOLD7  29672  nfsb4tw2AUXOLD7  29673
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