Theorem sp 1759

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 2073.

This theorem shows that our obsolete axiom ax-4 2185 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 1757. It is thought the best we can do using only Tarski's axioms is spw 1702. (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

Step	Hyp	Ref	Expression
1		alex 1578	. 2 |- ( A. x ph <-> -. E. x -. ph )
2		19.8a 1758	. . 3 |- ( -. ph -> E. x -. ph )
3	2	con1i 123	. 2 |- ( -. E. x -. ph -> ph )
4	1, 3	sylbi 188	1 |- ( A. x ph -> ph )

Syntax hints:   -. wn 3   -> wi 4   A.wal 1546   E.wex 1547

This theorem is referenced by:  ax5o  1761  ax6o  1762  spi  1765  sps  1766  spsd  1767  19.8aOLD  1768  19.21bi  1770  nfr  1773  19.3  1787  hbnOLD  1798  hba1OLD  1801  hbimdOLD  1831  spimehOLD  1836  equsalhwOLD  1857  19.21hOLD  1858  19.12  1865  19.12OLD  1866  nfald  1867  cbv3hvOLD  1875  19.21tOLD  1882  19.38OLD  1891  spimtOLD  1954  ax12olem3OLD  1979  ax12  1985  ax12OLD  1986  dvelimvOLD  1994  ax9OLD  1999  hbae  2005  equveliOLD  2043  ax11b  2048  sb2  2072  a16gb  2099  dfsb2  2104  nfsb4t  2129  sb56  2147  sb6  2148  sbal1  2176  exsb  2180  ax4  2195  mo  2276  mopick  2316  2eu1  2334  axi4  2375  axi5r  2376  nfcr  2532  rsp  2726  ceqex  3026  abidnf  3063  mob2  3074  csbie2t  3255  sbcnestgf  3258  mpteq12f  4245  axrep2  4282  axnulALT  4296  dtru  4350  copsex2t  4403  ssopab2  4440  eusv1  4676  alxfr  4695  iota1  5391  dffv2  5755  fiint  7342  isf32lem9  8197  nd3  8420  axrepnd  8425  axpowndlem2  8429  axacndlem4  8441  fiinopn  16929  ex-natded9.26-2  21681  relexpindlem  25092  fundmpss  25336  frmin  25456  wfrlem5  25474  frrlem5  25499  mbfresfi  26152  prtlem14  26613  setindtr  26985  pm11.57  27456  pm11.59  27458  ax4567to6  27472  ax4567to7  27473  ax10ext  27474  iotain  27485  pm14.123b  27494  eubi  27504  rexsb  27813  ssralv2  28326  19.41rg  28348  hbexg  28354  a9e2ndeq  28357  ssralv2VD  28687  19.41rgVD  28723  hbimpgVD  28725  hbexgVD  28727  a9e2eqVD  28728  a9e2ndeqVD  28730  vk15.4jVD  28735  a9e2ndeqALT  28753  bnj1294  28895  bnj570  28982  bnj953  29016  bnj1204  29087  bnj1388  29108  19.12vAUX7  29160  ax12olem3aAUX7  29163  dvelimvNEW7  29168  ax9NEW7  29174  hbaewAUX7  29184  spimtNEW7  29213  equveliNEW7  29232  sb2NEW7  29241  a16gbNEW7  29251  nfsb4twAUX7  29280  sb56NEW7  29297  sb6NEW7  29298  exsbNEW7  29300  sbal1NEW7  29316  ax11bNEW7  29323  dfsb2NEW7  29339  ax7w1AUX7  29345  hbaew0AUX7  29347  ax7w7AUX7  29353  ax7w4AUX7  29358  19.12OLD7  29370  hbaeOLD7  29392  nfsb4tOLD7  29429  nfsb4tw2AUXOLD7  29430

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 1662  ax-8 1683  ax-11 1757

This theorem depends on definitions:  df-bi 178  df-ex 1548