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

Metamath Proof Explorer

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