Theorem ercl2

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	ercl2	$$⊢\phi \to B\in X$$

Proof

Step	Hyp	Ref	Expression
1		ersym.1	$$⊢\phi \to R\mathrm{Er}X$$
2		ersym.2	$$⊢\phi \to ARB$$
3	1 2	ersym	$$⊢\phi \to BRA$$
4	1 3	ercl	$$⊢\phi \to B\in X$$