Theorem ax6evr 1731

Description: A commuted form of a9ev 1723. 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	⊢ ∃𝑥 𝑦 = 𝑥

Distinct variable group:   𝑥,𝑦

Proof of Theorem ax6evr

Step	Hyp	Ref	Expression
1		a9ev 1723	. 2 ⊢ ∃𝑥 𝑥 = 𝑦
2		equcomi 1730	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
3	1, 2	eximii 1628	1 ⊢ ∃𝑥 𝑦 = 𝑥

Syntax hints:  ∃wex 1518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1473  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560

This theorem depends on definitions:  df-bi 117

This theorem is referenced by: (None)