Theorem ax5e 1942

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1568  ∃wex 1809

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

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  ax5ea  1943  exlimiv  1960  exlimdv  1963  19.21v  1969  19.23v  1972  19.36imv  1975  19.41v  1979  19.9v  2014  aeveq  2088  sbv  2122  sbequ2  2285  mo4  2594  rspn0  4312  relopabi  5811  lfuhgr3  35593  bj-cbveximdv  37237  bj-spvw  37238  bj-spvew  37239  bj-exextruan  37241  bj-cbvexvv  37243  bj-cbval  37249  bj-cbvexivw  37276  bj-eqs  37279  bj-nnfv  37374  bj-snsetex  37580  bj-snglss  37587  bj-axseprep  37692  bj-axreprepsep  37693  topdifinffinlem  37974  wl-eujustlem1  38224  ac6s6f  38803  ismnushort  44994  fnchoice  45732  ormklocald  47573  natlocalincr  47575