Theorem ax5e 1935

Description: A rephrasing of ax-5 1933 using the existential quantifier. (Contributed by Wolf Lammen, 4-Dec-2017.)

Assertion

Ref	Expression
ax5e	⊢ (∃𝑥𝜑 → 𝜑)

Distinct variable group:   𝜑,𝑥

Proof of Theorem ax5e

Step	Hyp	Ref	Expression
1		ax-5 1933	. 2 ⊢ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)
2		eximal 1805	. 2 ⊢ ((∃𝑥𝜑 → 𝜑) ↔ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
3	1, 2	mpbir 234	1 ⊢ (∃𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1561  ∃wex 1802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-ex 1803

This theorem is referenced by:  ax5ea  1936  exlimiv  1953  exlimdv  1956  19.21v  1962  19.23v  1965  19.36imv  1968  19.41v  1972  19.9v  2007  aeveq  2081  sbv  2124  sbequ2  2287  mo4  2596  rspn0  4312  relopabi  5800  lfuhgr3  35483  bj-cbveximdv  37118  bj-spvw  37119  bj-spvew  37120  bj-exextruan  37122  bj-cbvexvv  37124  bj-cbval  37130  bj-cbvexivw  37157  bj-eqs  37160  bj-nnfv  37255  bj-snsetex  37460  bj-snglss  37467  bj-axseprep  37571  bj-axreprepsep  37572  topdifinffinlem  37853  wl-eujustlem1  38103  ac6s6f  38684  ismnushort  44875  fnchoice  45607  ormklocald  47448  natlocalincr  47450