Theorem ax6evr 1636

Description: A commuted form of a9ev 1630. The naming reflects how axioms were numbered in the Metamath Proof Explorer as of 2020 (a numbering which we eventually plan to adopt here too, but until this happens everywhere only some theorems will have it). (Contributed by BJ, 7-Dec-2020.)

Assertion

Ref	Expression
ax6evr	|- E. x y = x

Distinct variable group:   x, y

Proof of Theorem ax6evr

Step	Hyp	Ref	Expression
1		a9ev 1630	. 2 |- E. x x = y
2		equcomi 1635	. 2 |- ( x = y -> y = x )
3	1, 2	eximii 1536	1 |- E. x y = x

Syntax hints:   E.wex 1424

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470

This theorem depends on definitions:  df-bi 115

This theorem is referenced by: (None)