Theorem sp 1990

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

This theorem shows that our obsolete axiom ax-c5 32688 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 1983. It is thought the best we can do using only Tarski's axioms is spw 1915. (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 1729	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		19.8a 1988	. . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
3	2	con1i 136	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑)
4	1, 3	sylbi 202	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1466  ∃wex 1692

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-12 1983

This theorem depends on definitions:  df-bi 192  df-ex 1693

This theorem is referenced by:  axc4  1991  axc7  1992  spi  1995  sps  1996  2sp  1997  spsd  1998  19.21bi  2000  nfr  2004  19.3  2019  axc16gb  2077  19.12  2085  nfald  2086  sb56  2129  ax13OLD  2189  hbae  2198  ax12  2224  ax12b  2228  sb2  2235  dfsb2  2256  sbequi  2258  nfsb4t  2272  exsb  2351  mo3  2390  mopick  2418  axi4  2476  axi5r  2477  nfcr  2638  rsp  2808  ceqex  3192  abidnf  3231  mob2  3242  sbcnestgf  3824  mpteq12f  4511  axrep2  4550  axnulALT  4564  dtru  4633  eusv1  4636  alxfr  4652  iota1  5611  dffv2  6005  fiint  7933  isf32lem9  8876  nd3  9099  axrepnd  9104  axpowndlem2  9108  axpowndlem3  9109  axacndlem4  9120  trclfvcotr  13233  relexpindlem  13286  fiinopn  20089  ex-natded9.26-2  26030  bnj1294  29781  bnj570  29868  bnj953  29902  bnj1204  29973  bnj1388  29994  frmin  30631  bj-hbxfrbi  31398  bj-ssbft  31437  bj-ssbequ2  31438  bj-ssbid2ALT  31441  bj-sb  31465  bj-spst  31467  bj-19.21bit  31468  bj-19.3t  31477  bj-sb2v  31546  bj-axrep2  31586  bj-dtru  31594  bj-hbaeb2  31602  bj-hbnaeb  31604  bj-sbsb  31621  bj-nfcsym  31678  bj-ax9  31682  exlimim  31965  exellim  31968  wl-aleq  32099  wl-equsal1i  32107  wl-sb8t  32111  wl-lem-exsb  32126  wl-lem-moexsb  32128  wl-mo2tf  32131  wl-eutf  32133  wl-mo2t  32135  wl-mo3t  32136  wl-sb8eut  32137  wl-ax11-lem2  32141  nfbii2  32638  prtlem14  32679  axc5  32698  setindtr  36119  pm11.57  37096  pm11.59  37098  axc5c4c711toc7  37112  axc5c4c711to11  37113  axc11next  37114  iotain  37125  eubi  37144  ssralv2  37244  19.41rg  37273  hbexg  37279  ax6e2ndeq  37282  ssralv2VD  37611  19.41rgVD  37647  hbimpgVD  37649  hbexgVD  37651  ax6e2eqVD  37652  ax6e2ndeqVD  37654  vk15.4jVD  37659  ax6e2ndeqALT  37676  rexsb  39109