Theorem ax5e 1912

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

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

This theorem is referenced by:  ax5ea  1913  exlimiv  1930  exlimdv  1933  19.21v  1939  19.23v  1942  19.36imv  1945  19.41v  1949  19.9v  1983  aeveq  2056  sbv  2088  sbequ2  2249  mo4  2565  rspn0  4331  relopabi  5801  lfuhgr3  35142  bj-cbvalim  36663  bj-cbvexim  36664  bj-cbvexivw  36690  bj-eqs  36693  bj-nnfv  36772  bj-snsetex  36981  bj-snglss  36988  topdifinffinlem  37365  ac6s6f  38197  ismnushort  44325  fnchoice  45053  ormklocald  46903  natlocalincr  46905