Theorem ax5e 1947

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

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

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

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

This theorem is used by:  ax5ea  1948  exlimiv  1965  exlimdv  1968  19.21v  1974  19.23v  1977  19.36imv  1980  19.41v  1984  19.9v  2019  aeveq  2093  sbv  2127  sbequ2  2288  mo4  2594  rspn0  4307  relopabiOLD  5807  lfuhgr3  29761  bj-cbveximdv  37724  bj-spvw  37725  bj-spvew  37726  bj-exextruan  37728  bj-cbvexvv  37730  bj-cbval  37736  bj-cbvexivw  37763  bj-eqs  37766  bj-nnfv  37861  bj-snsetex  38067  bj-snglss  38074  bj-axseprep  38194  bj-axreprepsep  38195  topdifinffinlem  38475  wl-eujustlem1  38725  ac6s6f  39308  ismnushort  45488  fnchoice  46262  ormklocald  48101