Theorem sp 1843

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

This theorem shows that our obsolete axiom ax-c5 2198 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 1838. It is thought the best we can do using only Tarski's axioms is spw 1791. (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 1632	. 2 |- ( A. x ph <-> -. E. x -. ph )
2		19.8a 1841	. . 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 1379   E.wex 1597

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-12 1838

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

This theorem is referenced by:  axc4  1844  axc7  1845  spi  1848  sps  1849  2sp  1850  spsd  1851  19.21bi  1853  nfr  1857  19.3  1872  ax16gb  1926  19.12  1934  nfald  1935  ax13  2031  hbae  2039  ax12b  2070  sb2  2077  dfsb2  2098  sbequi  2100  nfsb4t  2114  sb56  2156  exsb  2196  axc5  2208  mo3  2307  mopick  2340  2eu1OLD  2361  axi4  2410  axi5r  2411  nfcr  2594  rsp  2807  ceqex  3214  abidnf  3252  mob2  3263  sbcnestgf  3822  mpteq12f  4510  axrep2  4547  axnulALT  4561  dtru  4625  eusv1  4628  alxfr  4647  iota1  5552  dffv2  5928  fiint  7796  isf32lem9  8741  nd3  8964  axrepnd  8969  axpowndlem2  8973  axpowndlem2OLD  8974  axpowndlem3  8975  axacndlem4  8988  fiinopn  19280  ex-natded9.26-2  25010  relexpindlem  28932  frmin  29294  wl-aleq  29960  wl-equsal1i  29968  wl-sb8t  29972  wl-lem-exsb  29987  wl-lem-moexsb  29989  wl-mo2t  29992  wl-mo3t  29993  wl-sb8eut  29994  wl-ax11-lem2  29998  nfbii2  30539  prtlem14  30587  setindtr  30938  pm11.57  31246  pm11.59  31248  axc5c4c711toc7  31262  axc5c4c711to11  31263  axc11next  31264  iotain  31275  eubi  31294  rexsb  32011  ssralv2  33029  19.41rg  33051  hbexg  33057  ax6e2ndeq  33060  ssralv2VD  33394  19.41rgVD  33430  hbimpgVD  33432  hbexgVD  33434  ax6e2eqVD  33435  ax6e2ndeqVD  33437  vk15.4jVD  33442  ax6e2ndeqALT  33459  bnj1294  33604  bnj570  33691  bnj953  33725  bnj1204  33796  bnj1388  33817  bj-hbxfrbi  33951  bj-spst  33977  bj-19.21bit  33978  bj-19.3t  33987  bj-ax16gb  34058  bj-sb2v  34066  bj-sb56  34082  bj-axrep2  34108  bj-dtru  34116  bj-hbaeb2  34124  bj-hbnaeb  34126  bj-nfcsym  34193  bj-ax9  34197