This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ax5e

Description: A rephrasing of ax-5 using the existential quantifier. (Contributed by Wolf Lammen, 4-Dec-2017)

		Ref	Expression
	Assertion	ax5e	$⊢ \exists x φ \to φ$

Step	Hyp	Ref	Expression
1		ax-5	$⊢ \neg φ \to \forall x \neg φ$
2		eximal	$⊢ (\exists x φ \to φ) \leftrightarrow (\neg φ \to \forall x \neg φ)$
3	1 2	mpbir	$⊢ \exists x φ \to φ$