Theorem sp 1911

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

This theorem shows that our obsolete axiom ax-c5 32422 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 1906. It is thought the best we can do using only Tarski's axioms is spw 1858. (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 1695	. 2 |- ( A. x ph <-> -. E. x -. ph )
2		19.8a 1909	. . 3 |- ( -. ph -> E. x -. ph )
3	2	con1i 133	. 2 |- ( -. E. x -. ph -> ph )
4	1, 3	sylbi 199	1 |- ( A. x ph -> ph )

Syntax hints:   -. wn 3   -> wi 4   A.wal 1436   E.wex 1660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-12 1906

This theorem depends on definitions:  df-bi 189  df-ex 1661

This theorem is referenced by:  axc4  1912  axc7  1913  spi  1916  sps  1917  2sp  1918  spsd  1919  19.21bi  1921  nfr  1925  19.3  1940  axc16gb  1999  19.12  2007  nfald  2008  ax13  2103  hbae  2111  ax12b  2142  sb2  2147  dfsb2  2168  sbequi  2170  nfsb4t  2184  sb56  2224  exsb  2264  mo3  2304  mopick  2332  2eu1OLD  2352  axi4  2392  axi5r  2393  nfcr  2576  rsp  2792  ceqex  3203  abidnf  3241  mob2  3252  sbcnestgf  3814  mpteq12f  4499  axrep2  4537  axnulALT  4551  dtru  4614  eusv1  4617  alxfr  4633  iota1  5578  dffv2  5953  fiint  7856  isf32lem9  8797  nd3  9020  axrepnd  9025  axpowndlem2  9029  axpowndlem3  9030  axacndlem4  9041  trclfvcotr  13071  relexpindlem  13124  fiinopn  19927  ex-natded9.26-2  25866  bnj1294  29635  bnj570  29722  bnj953  29756  bnj1204  29827  bnj1388  29848  frmin  30485  bj-hbxfrbi  31213  bj-spst  31240  bj-19.21bit  31241  bj-19.3t  31250  bj-axc16gb  31322  bj-sb2v  31330  bj-sb56  31346  bj-axrep2  31372  bj-dtru  31380  bj-hbaeb2  31388  bj-hbnaeb  31390  bj-nfcsym  31461  bj-ax9  31465  exlimim  31706  exellim  31709  wl-aleq  31830  wl-equsal1i  31838  wl-sb8t  31842  wl-lem-exsb  31857  wl-lem-moexsb  31859  wl-mo2tf  31862  wl-eutf  31864  wl-mo2t  31866  wl-mo3t  31867  wl-sb8eut  31868  wl-ax12  31875  wl-ax11-lem2  31878  nfbii2  32364  prtlem14  32412  axc5  32432  setindtr  35847  pm11.57  36645  pm11.59  36647  axc5c4c711toc7  36661  axc5c4c711to11  36662  axc11next  36663  iotain  36674  eubi  36693  ssralv2  36794  19.41rg  36823  hbexg  36829  ax6e2ndeq  36832  ssralv2VD  37172  19.41rgVD  37208  hbimpgVD  37210  hbexgVD  37212  ax6e2eqVD  37213  ax6e2ndeqVD  37215  vk15.4jVD  37220  ax6e2ndeqALT  37237  rexsb  38350