Metamath Proof Explorer

Theorem ercl

Description: Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypotheses ersym.1 φ R Er X
ersym.2 φ A R B
Assertion ercl φ A X


Step Hyp Ref Expression
1 ersym.1 φ R Er X
2 ersym.2 φ A R B
3 errel R Er X Rel R
4 1 3 syl φ Rel R
5 releldm Rel R A R B A dom R
6 4 2 5 syl2anc φ A dom R
7 erdm R Er X dom R = X
8 1 7 syl φ dom R = X
9 6 8 eleqtrd φ A X