Theorem ax5e 1916

Description: A rephrasing of ax-5 1914 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 1914	. 2 ⊢ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)
2		eximal 1786	. 2 ⊢ ((∃𝑥𝜑 → 𝜑) ↔ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
3	1, 2	mpbir 230	1 ⊢ (∃𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1537  ∃wex 1783

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

This theorem depends on definitions:  df-bi 206  df-ex 1784

This theorem is referenced by:  ax5ea  1917  exlimiv  1934  exlimdv  1937  19.21v  1943  19.23v  1946  19.36imv  1949  19.36imvOLD  1950  19.41v  1954  19.9v  1988  aeveq  2060  sbv  2092  sbequ2  2244  mo4  2566  rspn0  4283  relopabi  5721  lfuhgr3  32981  bj-cbvalim  34753  bj-cbvexim  34754  bj-cbvexivw  34780  bj-eqs  34783  bj-nnfv  34863  bj-snsetex  35080  bj-snglss  35087  topdifinffinlem  35445  ac6s6f  36258  ismnushort  41808  fnchoice  42461