Theorem eqvrelthi

Description: Basic property of equivalence relations. Part of Lemma 3N of Enderton p. 57. (Contributed by NM, 30-Jul-1995) (Revised by Mario Carneiro, 9-Jul-2014) (Revised by Peter Mazsa, 2-Jun-2019)

	Ref	Expression
Hypotheses	eqvrelthi.1	$$⊢\phi \to EqvRelR$$
	eqvrelthi.2	$$⊢\phi \to ARB$$
Assertion	eqvrelthi	$$⊢\phi \to \left[A\right]R=\left[B\right]R$$

Proof

Step	Hyp	Ref	Expression
1		eqvrelthi.1	$$⊢\phi \to EqvRelR$$
2		eqvrelthi.2	$$⊢\phi \to ARB$$
3	1 2	eqvrelcl	$$⊢\phi \to A\in \mathrm{dom}R$$
4	1 3	eqvrelth	$$⊢\phi \to \left(ARB\leftrightarrow \left[A\right]R=\left[B\right]R\right)$$
5	2 4	mpbid	$$⊢\phi \to \left[A\right]R=\left[B\right]R$$