Theorem ax6evr

Description: A commuted form of ax6ev . (Contributed by BJ, 7-Dec-2020)

	Ref	Expression
Assertion	ax6evr	|- E. x y = x

Proof

Step	Hyp	Ref	Expression
1		ax6ev	|- E. x x = y
2		equcomiv	|- ( x = y -> y = x )
3	1 2	eximii	|- E. x y = x