Theorem ercl

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

	Ref	Expression
Hypotheses	ersym.1	$$⊢\phi \to R\mathrm{Er}X$$
	ersym.2	$$⊢\phi \to ARB$$
Assertion	ercl	$$⊢\phi \to A\in X$$

Proof

Step	Hyp	Ref	Expression
1		ersym.1	$$⊢\phi \to R\mathrm{Er}X$$
2		ersym.2	$$⊢\phi \to ARB$$
3		errel	$$⊢R\mathrm{Er}X\to \mathrm{Rel}R$$
4	1 3	syl	$$⊢\phi \to \mathrm{Rel}R$$
5		releldm	$$⊢\left(\mathrm{Rel}R\wedge ARB\right)\to A\in \mathrm{dom}R$$
6	4 2 5	syl2anc	$$⊢\phi \to A\in \mathrm{dom}R$$
7		erdm	$$⊢R\mathrm{Er}X\to \mathrm{dom}R=X$$
8	1 7	syl	$$⊢\phi \to \mathrm{dom}R=X$$
9	6 8	eleqtrd	$$⊢\phi \to A\in X$$