Theorem ax5ea

Description: If a formula holds for some value of a variable not occurring in it, then it holds for all values of that variable. (Contributed by BJ, 28-Dec-2020)

	Ref	Expression
Assertion	ax5ea	$$⊢\exists x\phi \to \forall x\phi$$

Proof

Step	Hyp	Ref	Expression
1		ax5e	$$⊢\exists x\phi \to \phi$$
2		ax-5	$$⊢\phi \to \forall x\phi$$
3	1 2	syl	$$⊢\exists x\phi \to \forall x\phi$$