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	|- ( E. x ph -> A. x ph )

Proof

Step	Hyp	Ref	Expression
1		ax5e	|- ( E. x ph -> ph )
2		ax-5	|- ( ph -> A. x ph )
3	1 2	syl	|- ( E. x ph -> A. x ph )