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

Theorem sp 1764
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 2092.

This theorem shows that our obsolete axiom ax-4 2214 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 1762. It is thought the best we can do using only Tarski's axioms is spw 1707. (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 1582 . 2  |-  ( A. x ph  <->  -.  E. x  -.  ph )
2 19.8a 1763 . . 3  |-  ( -. 
ph  ->  E. x  -.  ph )
32con1i 124 . 2  |-  ( -. 
E. x  -.  ph  ->  ph )
41, 3sylbi 189 1  |-  ( A. x ph  ->  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1550   E.wex 1551
This theorem is referenced by:  ax5o  1766  ax6o  1767  spi  1770  sps  1771  spsd  1772  19.8aOLD  1773  19.21bi  1775  nfr  1778  19.3  1792  hbnOLD  1803  hba1OLD  1806  hbimdOLD  1836  spimehOLD  1841  equsalhwOLD  1862  19.21hOLD  1863  19.12  1870  19.12OLD  1871  nfald  1872  cbv3hvOLD  1880  19.21tOLD  1887  19.38OLD  1896  spimtOLD  1957  cbv1h  1975  ax12olem3OLD  2014  ax12  2020  ax12OLD  2021  dvelimvOLD  2029  ax9OLD  2034  hbae  2041  hbaeOLD  2042  a16gb  2053  ax11b  2083  equveliOLD  2087  sb2  2091  dfsb2  2110  nfsb4t  2129  nfsb4tOLD  2130  sb56  2176  sb6  2177  sbal1  2205  exsb  2209  ax4  2224  mo  2305  mopick  2345  2eu1  2363  axi4  2410  axi5r  2411  nfcr  2566  rsp  2768  ceqex  3068  abidnf  3105  mob2  3116  csbie2t  3297  sbcnestgf  3300  mpteq12f  4288  axrep2  4325  axnulALT  4339  dtru  4393  copsex2t  4446  ssopab2  4483  eusv1  4720  alxfr  4739  iota1  5435  dffv2  5799  fiint  7386  isf32lem9  8246  nd3  8469  axrepnd  8474  axpowndlem2  8478  axacndlem4  8490  fiinopn  16979  ex-natded9.26-2  21733  relexpindlem  25144  fundmpss  25395  frmin  25522  wfrlem5  25547  frrlem5  25591  wl-aleq  26240  mbfresfi  26265  prtlem14  26737  setindtr  27109  pm11.57  27579  pm11.59  27581  ax4567to6  27595  ax4567to7  27596  ax10ext  27597  iotain  27608  pm14.123b  27617  eubi  27627  rexsb  27936  ssralv2  28689  19.41rg  28711  hbexg  28717  a9e2ndeq  28720  ssralv2VD  29052  19.41rgVD  29088  hbimpgVD  29090  hbexgVD  29092  a9e2eqVD  29093  a9e2ndeqVD  29095  vk15.4jVD  29100  a9e2ndeqALT  29117  bnj1294  29263  bnj570  29350  bnj953  29384  bnj1204  29455  bnj1388  29476  19.12vAUX7  29528  ax12olem3aAUX7  29531  dvelimvNEW7  29536  ax9NEW7  29542  hbaewAUX7  29552  spimtNEW7  29581  equveliNEW7  29602  sb2NEW7  29611  a16gbNEW7  29621  nfsb4twAUX7  29650  sb56NEW7  29670  sb6NEW7  29671  exsbNEW7  29673  sbal1NEW7  29689  ax11bNEW7  29696  dfsb2NEW7  29712  ax7w1AUX7  29719  hbaew0AUX7  29721  ax7w7AUX7  29727  ax7w4AUX7  29732  ax7w10AUX7  29736  ax7w11AUX7  29737  ax7w18AUX7  29751  19.12OLD7  29760  hbaeOLD7  29782  nfsb4tOLD7  29819  nfsb4tw2AUXOLD7  29820
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator