Theorem sp 1859

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

This theorem shows that our obsolete axiom ax-c5 2214 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 1854. It is thought the best we can do using only Tarski's axioms is spw 1807. (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

Proof of Theorem sp

Step	Hyp	Ref	Expression
1		alex 1647	. 2
2		19.8a 1857	. . 3
3	2	con1i 129	. 2
4	1, 3	sylbi 195	1

Syntax hints:  -.wn 3  ->wi 4  A.wal 1393  E.wex 1612

This theorem is referenced by:  axc4  1860  axc7  1861  spi  1864  sps  1865  2sp  1866  spsd  1867  19.21bi  1869  nfr  1873  19.3  1888  ax16gb  1942  19.12  1950  nfald  1951  ax13  2047  hbae  2055  ax12b  2086  sb2  2093  dfsb2  2114  sbequi  2116  nfsb4t  2130  sb56  2172  exsb  2212  axc5  2224  mo3  2323  mopick  2356  2eu1OLD  2377  axi4  2426  axi5r  2427  nfcr  2610  rsp  2823  ceqex  3230  abidnf  3268  mob2  3279  sbcnestgf  3839  mpteq12f  4528  axrep2  4565  axnulALT  4579  dtru  4643  eusv1  4646  alxfr  4665  iota1  5570  dffv2  5946  fiint  7817  isf32lem9  8762  nd3  8985  axrepnd  8990  axpowndlem2  8994  axpowndlem2OLD  8995  axpowndlem3  8996  axacndlem4  9009  fiinopn  19410  ex-natded9.26-2  25141  relexpindlem  29062  frmin  29322  wl-aleq  29988  wl-equsal1i  29996  wl-sb8t  30000  wl-lem-exsb  30015  wl-lem-moexsb  30017  wl-mo2t  30020  wl-mo3t  30021  wl-sb8eut  30022  wl-ax11-lem2  30026  nfbii2  30567  prtlem14  30615  setindtr  30966  pm11.57  31295  pm11.59  31297  axc5c4c711toc7  31311  axc5c4c711to11  31312  axc11next  31313  iotain  31324  eubi  31343  rexsb  32173  ssralv2  33301  19.41rg  33323  hbexg  33329  ax6e2ndeq  33332  ssralv2VD  33666  19.41rgVD  33702  hbimpgVD  33704  hbexgVD  33706  ax6e2eqVD  33707  ax6e2ndeqVD  33709  vk15.4jVD  33714  ax6e2ndeqALT  33731  bnj1294  33876  bnj570  33963  bnj953  33997  bnj1204  34068  bnj1388  34089  bj-hbxfrbi  34216  bj-spst  34242  bj-19.21bit  34243  bj-19.3t  34252  bj-ax16gb  34325  bj-sb2v  34333  bj-sb56  34349  bj-axrep2  34375  bj-dtru  34383  bj-hbaeb2  34391  bj-hbnaeb  34393  bj-nfcsym  34460  bj-ax9  34464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854

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