Theorem ax5e 1931

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1557  ∃wex 1798

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

This theorem depends on definitions:  df-bi 209  df-ex 1799

This theorem is referenced by:  ax5ea  1932  exlimiv  1949  exlimdv  1952  19.21v  1958  19.23v  1961  19.36imv  1964  19.41v  1968  19.9v  2003  aeveq  2077  sbv  2120  sbequ2  2283  mo4  2592  rspn0  4308  relopabi  5793  lfuhgr3  35434  bj-cbveximdv  37070  bj-spvw  37071  bj-spvew  37072  bj-exextruan  37074  bj-cbvexvv  37076  bj-cbval  37082  bj-cbvexivw  37109  bj-eqs  37112  bj-nnfv  37207  bj-snsetex  37412  bj-snglss  37419  bj-axseprep  37523  bj-axreprepsep  37524  topdifinffinlem  37805  wl-eujustlem1  38055  ac6s6f  38636  ismnushort  44841  fnchoice  45573  ormklocald  47414  natlocalincr  47416