Theorem sp 1877

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

This theorem shows that our obsolete axiom ax-c5 35062 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 auxiliary axiom scheme ax-12 1872. It is thought the best we can do using only Tarski's axioms is spw 1825. (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 1662	. 2 |- ( A. x ph <-> -. E. x -. ph )
2		19.8a 1875	. . 3 |- ( -. ph -> E. x -. ph )
3	2	con1i 129	. 2 |- ( -. E. x -. ph -> ph )
4	1, 3	sylbi 195	1 |- ( A. x ph -> ph )

Syntax hints:   -. wn 3   -> wi 4   A.wal 1397   E.wex 1627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-12 1872

This theorem depends on definitions:  df-bi 185  df-ex 1628

This theorem is referenced by:  axc4  1878  axc7  1879  spi  1882  sps  1883  2sp  1884  spsd  1885  19.21bi  1887  nfr  1891  19.3  1906  ax16gb  1960  19.12  1968  nfald  1969  ax13  2063  hbae  2071  ax12b  2102  sb2  2107  dfsb2  2128  sbequi  2130  nfsb4t  2144  sb56  2186  exsb  2226  mo3  2268  mopick  2297  2eu1OLD  2318  axi4  2361  axi5r  2362  nfcr  2545  rsp  2758  ceqex  3168  abidnf  3206  mob2  3217  sbcnestgf  3775  mpteq12f  4456  axrep2  4493  axnulALT  4507  dtru  4569  eusv1  4572  alxfr  4588  iota1  5487  dffv2  5860  fiint  7730  isf32lem9  8672  nd3  8895  axrepnd  8900  axpowndlem2  8904  axpowndlem3  8905  axacndlem4  8917  trclfvcotr  12866  relexpindlem  12917  fiinopn  19514  ex-natded9.26-2  25283  frmin  29523  wl-aleq  30189  wl-equsal1i  30197  wl-sb8t  30201  wl-lem-exsb  30216  wl-lem-moexsb  30218  wl-mo2t  30221  wl-mo3t  30222  wl-sb8eut  30223  wl-ax11-lem2  30227  nfbii2  30769  prtlem14  30817  setindtr  31168  pm11.57  31499  pm11.59  31501  axc5c4c711toc7  31515  axc5c4c711to11  31516  axc11next  31517  iotain  31528  eubi  31547  rexsb  32374  ssralv2  33669  19.41rg  33698  hbexg  33704  ax6e2ndeq  33707  ssralv2VD  34048  19.41rgVD  34084  hbimpgVD  34086  hbexgVD  34088  ax6e2eqVD  34089  ax6e2ndeqVD  34091  vk15.4jVD  34096  ax6e2ndeqALT  34113  bnj1294  34258  bnj570  34345  bnj953  34379  bnj1204  34450  bnj1388  34471  bj-hbxfrbi  34598  bj-spst  34624  bj-19.21bit  34625  bj-19.3t  34634  bj-ax16gb  34707  bj-sb2v  34715  bj-sb56  34731  bj-axrep2  34757  bj-dtru  34765  bj-hbaeb2  34773  bj-hbnaeb  34775  bj-nfcsym  34842  bj-ax9  34846  axc5  35072