Theorem sp 1799

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

This theorem shows that our obsolete axiom ax-c5 2194 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 1794. It is thought the best we can do using only Tarski's axioms is spw 1747. (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 1618	. 2 |- ( A. x ph <-> -. E. x -. ph )
2		19.8a 1797	. . 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 1368   E.wex 1587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794

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

This theorem is referenced by:  axc4  1800  axc7  1801  spi  1804  sps  1805  2sp  1806  spsd  1807  19.21bi  1809  nfr  1812  19.3  1827  ax16gb  1880  19.12  1888  nfald  1889  ax13  2007  hbae  2015  ax12b  2046  sb2  2053  dfsb2  2074  sbequi  2076  nfsb4t  2090  sb56  2141  sb6OLD  2143  sbal1OLD  2181  exsb  2190  axc5  2204  mo3  2307  moOLD  2314  mopick  2348  2eu1OLD  2374  axi4  2423  axi5r  2424  nfcr  2607  rsp  2894  ceqex  3197  abidnf  3235  mob2  3246  sbcnestgf  3802  mpteq12f  4479  axrep2  4516  axnulALT  4530  dtru  4594  eusv1  4597  alxfr  4616  iota1  5506  dffv2  5876  fiint  7702  isf32lem9  8644  nd3  8867  axrepnd  8872  axpowndlem2  8876  axpowndlem2OLD  8877  axpowndlem3  8878  axacndlem4  8891  fiinopn  18649  ex-natded9.26-2  23799  relexpindlem  27505  frmin  27867  wl-aleq  28532  wl-equsal1i  28540  wl-sb8t  28544  wl-lem-exsb  28559  wl-lem-moexsb  28561  wl-mo2t  28564  wl-mo3t  28565  wl-sb8eut  28566  wl-ax11-lem2  28570  nfbii2  29139  prtlem14  29187  setindtr  29541  pm11.57  29810  pm11.59  29812  axc5c4c711toc7  29826  axc5c4c711to11  29827  axc11next  29828  iotain  29839  eubi  29858  rexsb  30160  ssralv2  31588  19.41rg  31611  hbexg  31617  ax6e2ndeq  31620  ssralv2VD  31954  19.41rgVD  31990  hbimpgVD  31992  hbexgVD  31994  ax6e2eqVD  31995  ax6e2ndeqVD  31997  vk15.4jVD  32002  ax6e2ndeqALT  32019  bnj1294  32163  bnj570  32250  bnj953  32284  bnj1204  32355  bnj1388  32376  bj-hbxfrbi  32510  bj-spst  32530  bj-19.21bit  32531  bj-19.3t  32540  bj-ax16gb  32612  bj-sb2v  32620  bj-sb56  32636  bj-axrep2  32662  bj-dtru  32670  bj-hbaeb  32678  bj-hbnaeb  32679  bj-nfcsym  32747  bj-ax9  32751