Theorem sp 1957

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). This corresponds to the axiom (T) of modal logic.

For the axiom of specialization presented in many logic textbooks, see theorem stdpc4 2202.

This theorem shows that our obsolete axiom ax-c5 32519 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 1950. It is thought the best we can do using only Tarski's axioms is spw 1884. (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 1706	. 2 |- ( A. x ph <-> -. E. x -. ph )
2		19.8a 1955	. . 3 |- ( -. ph -> E. x -. ph )
3	2	con1i 134	. 2 |- ( -. E. x -. ph -> ph )
4	1, 3	sylbi 200	1 |- ( A. x ph -> ph )

Syntax hints:   -. wn 3   -> wi 4   A.wal 1450   E.wex 1671

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950

This theorem depends on definitions:  df-bi 190  df-ex 1672

This theorem is referenced by:  axc4  1958  axc7  1959  spi  1962  sps  1963  2sp  1964  spsd  1965  19.21bi  1967  nfr  1971  19.3  1986  axc16gb  2044  19.12  2052  nfald  2053  sb56  2096  ax13  2155  hbae  2164  ax12  2190  ax12b  2194  sb2  2201  dfsb2  2222  sbequi  2224  nfsb4t  2238  exsb  2317  mo3  2356  mopick  2384  axi4  2442  axi5r  2443  nfcr  2604  rsp  2773  ceqex  3157  abidnf  3195  mob2  3206  sbcnestgf  3788  mpteq12f  4472  axrep2  4510  axnulALT  4524  dtru  4592  eusv1  4595  alxfr  4611  iota1  5567  dffv2  5953  fiint  7866  isf32lem9  8809  nd3  9032  axrepnd  9037  axpowndlem2  9041  axpowndlem3  9042  axacndlem4  9053  trclfvcotr  13150  relexpindlem  13203  fiinopn  20008  ex-natded9.26-2  25949  bnj1294  29701  bnj570  29788  bnj953  29822  bnj1204  29893  bnj1388  29914  frmin  30551  bj-hbxfrbi  31280  bj-ssbft  31319  bj-ssbequ2  31320  bj-ssbid2ALT  31323  bj-spst  31348  bj-19.21bit  31349  bj-19.3t  31358  bj-axc16gb  31423  bj-sb2v  31431  bj-axrep2  31470  bj-dtru  31478  bj-hbaeb2  31486  bj-hbnaeb  31488  bj-sbsb  31505  bj-nfcsym  31562  bj-ax9  31566  exlimim  31814  exellim  31817  wl-aleq  31938  wl-equsal1i  31946  wl-sb8t  31950  wl-lem-exsb  31965  wl-lem-moexsb  31967  wl-mo2tf  31970  wl-eutf  31972  wl-mo2t  31974  wl-mo3t  31975  wl-sb8eut  31976  wl-ax11-lem2  31980  nfbii2  32466  prtlem14  32510  axc5  32529  setindtr  35950  pm11.57  36809  pm11.59  36811  axc5c4c711toc7  36825  axc5c4c711to11  36826  axc11next  36827  iotain  36838  eubi  36857  ssralv2  36958  19.41rg  36987  hbexg  36993  ax6e2ndeq  36996  ssralv2VD  37326  19.41rgVD  37362  hbimpgVD  37364  hbexgVD  37366  ax6e2eqVD  37367  ax6e2ndeqVD  37369  vk15.4jVD  37374  ax6e2ndeqALT  37391  rexsb  38734