Theorem sp 2184

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

This theorem shows that our obsolete axiom ax-c5 38881 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 2178. It is thought the best we can do using only Tarski's axioms is spw 2034. Also see spvw 1981 where 𝑥 and 𝜑 are disjoint, using fewer axioms. (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 1826	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		19.8a 2182	. . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
3	2	con1i 147	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑)
4	1, 3	sylbi 217	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1538  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  spi  2185  sps  2186  2sp  2187  spsd  2188  19.21bi  2190  19.3t  2202  19.3  2203  19.9d  2204  sb4av  2245  sbequ2  2250  axc16gb  2263  axc7  2316  axc4  2320  19.12  2326  exsb  2357  ax12  2421  ax12b  2422  ax13ALT  2423  hbae  2429  sb4a  2478  dfsb2  2491  nfsb4t  2497  mo3  2557  mopick  2618  axi4  2692  axi5r  2693  nfcrALT  2882  rsp  3217  ceqex  3609  elrab3t  3649  abidnf  3664  mob2  3677  sbcnestgfw  4374  sbcnestgf  4379  ralidm  4465  mpteq12f  5180  axrep2  5224  axnulALT  5246  eusv1  5333  alxfr  5349  axprlem4OLD  5371  axprlem5OLD  5372  iota1  6465  dffv2  6922  fiint  9235  fiintOLD  9236  isf32lem9  10274  nd3  10502  axrepnd  10507  axpowndlem2  10511  axpowndlem3  10512  axacndlem4  10523  trclfvcotr  14935  relexpindlem  14989  fiinopn  22805  ex-natded9.26-2  30383  bnj1294  34803  bnj570  34891  bnj953  34925  bnj1204  34998  bnj1388  35019  in-ax8  36217  ss-ax8  36218  bj-ssbid2ALT  36656  bj-sb  36680  bj-spst  36682  bj-19.21bit  36683  bj-substax12  36714  bj-hbaeb2  36811  bj-hbnaeb  36813  bj-sbsb  36830  bj-nfcsym  36892  exlimim  37335  exellim  37337  difunieq  37367  wl-aleq  37528  wl-equsal1i  37537  wl-sb8t  37545  wl-2spsbbi  37558  wl-lem-exsb  37559  wl-lem-moexsb  37561  wl-mo2tf  37564  wl-eutf  37566  wl-mo2t  37568  wl-mo3t  37569  wl-sb8eut  37571  wl-ax11-lem2  37579  mopickr  38350  prtlem14  38872  axc5  38891  setindtr  43017  unielss  43211  ismnushort  44294  pm11.57  44382  pm11.59  44384  axc5c4c711toc7  44397  axc5c4c711to11  44398  axc11next  44399  eubiOLD  44429  ssralv2  44525  19.41rg  44544  hbexg  44550  ax6e2ndeq  44553  ssralv2VD  44859  19.41rgVD  44895  hbimpgVD  44897  hbexgVD  44899  ax6e2eqVD  44900  ax6e2ndeqVD  44902  vk15.4jVD  44907  ax6e2ndeqALT  44924  rexsb  47103  ichnfimlem  47467  setrec1lem4  49695