Theorem eqvrelcl

Description: Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015) (Revised by Peter Mazsa, 2-Jun-2019)

	Ref	Expression
Hypotheses	eqvrelcl.1	$$⊢\phi \to EqvRelR$$
	eqvrelcl.2	$$⊢\phi \to ARB$$
Assertion	eqvrelcl	$$⊢\phi \to A\in \mathrm{dom}R$$

Proof

Step	Hyp	Ref	Expression
1		eqvrelcl.1	$$⊢\phi \to EqvRelR$$
2		eqvrelcl.2	$$⊢\phi \to ARB$$
3		eqvrelrel	$$⊢EqvRelR\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$$