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  29733  bj-cbveximdv  37625  bj-spvw  37626  bj-spvew  37627  bj-exextruan  37629  bj-cbvexvv  37631  bj-cbval  37637  bj-cbvexivw  37664  bj-eqs  37667  bj-nnfv  37762  bj-snsetex  37968  bj-snglss  37975  bj-axseprep  38082  bj-axreprepsep  38083  topdifinffinlem  38363  wl-eujustlem1  38613  ac6s6f  39198  ismnushort  45378  fnchoice  46139  ormklocald  47979