Metamath Proof Explorer

Theorem ax6er

Description: Commuted form of ax6e . (Could be placed right after ax6e ). (Contributed by BJ, 15-Sep-2018)

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

Proof

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