Theorem ax5e 1944

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1567  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-5 1942

This proof depends on definitions:  df-bi 210  df-ex 1812

This theorem is used by:  ax5ea  1945  exlimiv  1962  exlimdv  1965  19.21v  1971  19.23v  1974  19.36imv  1977  19.41v  1981  19.9v  2016  aeveq  2090  sbv  2124  sbequ2  2284  mo4  2591  rspn0  4303  relopabi  5799  lfuhgr3  29729  bj-cbveximdv  37608  bj-spvw  37609  bj-spvew  37610  bj-exextruan  37612  bj-cbvexvv  37614  bj-cbval  37620  bj-cbvexivw  37647  bj-eqs  37650  bj-nnfv  37745  bj-snsetex  37951  bj-snglss  37958  bj-axseprep  38065  bj-axreprepsep  38066  topdifinffinlem  38346  wl-eujustlem1  38596  ac6s6f  39181  ismnushort  45361  fnchoice  46122  ormklocald  47962