Theorem sp 1808

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

This theorem shows that our obsolete axiom ax-c5 2207 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 1803. It is thought the best we can do using only Tarski's axioms is spw 1756. (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 1627	. 2 |- ( A. x ph <-> -. E. x -. ph )
2		19.8a 1806	. . 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 1377   E.wex 1596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803

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

This theorem is referenced by:  axc4  1809  axc7  1810  spi  1813  sps  1814  2sp  1815  spsd  1816  19.21bi  1818  nfr  1821  19.3  1836  ax16gb  1889  19.12  1897  nfald  1898  ax13  2020  hbae  2028  ax12b  2059  sb2  2066  dfsb2  2087  sbequi  2089  nfsb4t  2103  sb56  2154  sb6OLD  2156  sbal1OLD  2194  exsb  2203  axc5  2217  mo3  2320  moOLD  2327  mopick  2361  2eu1OLD  2387  axi4  2436  axi5r  2437  nfcr  2620  rsp  2830  ceqex  3234  abidnf  3272  mob2  3283  sbcnestgf  3839  mpteq12f  4523  axrep2  4560  axnulALT  4574  dtru  4638  eusv1  4641  alxfr  4660  iota1  5565  dffv2  5941  fiint  7798  isf32lem9  8742  nd3  8965  axrepnd  8970  axpowndlem2  8974  axpowndlem2OLD  8975  axpowndlem3  8976  axacndlem4  8989  fiinopn  19217  ex-natded9.26-2  24915  relexpindlem  28813  frmin  29175  wl-aleq  29841  wl-equsal1i  29849  wl-sb8t  29853  wl-lem-exsb  29868  wl-lem-moexsb  29870  wl-mo2t  29873  wl-mo3t  29874  wl-sb8eut  29875  wl-ax11-lem2  29879  nfbii2  30398  prtlem14  30446  setindtr  30797  pm11.57  31100  pm11.59  31102  axc5c4c711toc7  31116  axc5c4c711to11  31117  axc11next  31118  iotain  31129  eubi  31148  rexsb  31867  ssralv2  32597  19.41rg  32620  hbexg  32626  ax6e2ndeq  32629  ssralv2VD  32963  19.41rgVD  32999  hbimpgVD  33001  hbexgVD  33003  ax6e2eqVD  33004  ax6e2ndeqVD  33006  vk15.4jVD  33011  ax6e2ndeqALT  33028  bnj1294  33172  bnj570  33259  bnj953  33293  bnj1204  33364  bnj1388  33385  bj-hbxfrbi  33521  bj-spst  33541  bj-19.21bit  33542  bj-19.3t  33551  bj-ax16gb  33623  bj-sb2v  33631  bj-sb56  33647  bj-axrep2  33673  bj-dtru  33681  bj-hbaeb2  33689  bj-hbnaeb  33691  bj-nfcsym  33758  bj-ax9  33762  frege58b  37109