Theorem sp 1937

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

This theorem shows that our obsolete axiom ax-c5 32455 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 1933. It is thought the best we can do using only Tarski's axioms is spw 1876. (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 1698	. 2 |- ( A. x ph <-> -. E. x -. ph )
2		19.8a 1935	. . 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 1442   E.wex 1663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-12 1933

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664

This theorem is referenced by:  axc4  1938  axc7  1939  spi  1942  sps  1943  2sp  1944  spsd  1945  19.21bi  1947  nfr  1951  19.3  1966  axc16gb  2025  19.12  2033  nfald  2034  sb56  2081  ax13  2141  hbae  2149  ax12b  2178  sb2  2183  dfsb2  2202  sbequi  2204  nfsb4t  2218  exsb  2297  mo3  2336  mopick  2364  axi4  2422  axi5r  2423  nfcr  2584  rsp  2754  ceqex  3169  abidnf  3207  mob2  3218  sbcnestgf  3784  mpteq12f  4479  axrep2  4517  axnulALT  4531  dtru  4594  eusv1  4597  alxfr  4613  iota1  5560  dffv2  5938  fiint  7848  isf32lem9  8791  nd3  9014  axrepnd  9019  axpowndlem2  9023  axpowndlem3  9024  axacndlem4  9035  trclfvcotr  13073  relexpindlem  13126  fiinopn  19931  ex-natded9.26-2  25870  bnj1294  29629  bnj570  29716  bnj953  29750  bnj1204  29821  bnj1388  29842  frmin  30480  bj-hbxfrbi  31216  bj-ssbft  31255  bj-ssbequ2  31256  bj-ssbid2ALT  31259  bj-spst  31282  bj-19.21bit  31283  bj-19.3t  31292  bj-axc16gb  31357  bj-sb2v  31365  bj-axrep2  31404  bj-dtru  31412  bj-hbaeb2  31420  bj-hbnaeb  31422  bj-nfcsym  31494  bj-ax9  31498  exlimim  31744  exellim  31747  wl-aleq  31868  wl-equsal1i  31876  wl-sb8t  31880  wl-lem-exsb  31895  wl-lem-moexsb  31897  wl-mo2tf  31900  wl-eutf  31902  wl-mo2t  31904  wl-mo3t  31905  wl-sb8eut  31906  wl-ax12  31913  wl-ax11-lem2  31916  nfbii2  32402  prtlem14  32446  axc5  32465  setindtr  35879  pm11.57  36739  pm11.59  36741  axc5c4c711toc7  36755  axc5c4c711to11  36756  axc11next  36757  iotain  36768  eubi  36787  ssralv2  36888  19.41rg  36917  hbexg  36923  ax6e2ndeq  36926  ssralv2VD  37263  19.41rgVD  37299  hbimpgVD  37301  hbexgVD  37303  ax6e2eqVD  37304  ax6e2ndeqVD  37306  vk15.4jVD  37311  ax6e2ndeqALT  37328  rexsb  38589