Theorem erth2

Description: Basic property of equivalence relations. Compare Theorem 73 of Suppes p. 82. Assumes membership of the second argument in the domain. (Contributed by NM, 30-Jul-1995) (Revised by Mario Carneiro, 6-Jul-2015)

	Ref	Expression
Hypotheses	erth2.1	$$⊢\phi \to R\mathrm{Er}X$$
	erth2.2	$$⊢\phi \to B\in X$$
Assertion	erth2	$$⊢\phi \to \left(ARB\leftrightarrow \left[A\right]R=\left[B\right]R\right)$$

Proof

Step	Hyp	Ref	Expression
1		erth2.1	$$⊢\phi \to R\mathrm{Er}X$$
2		erth2.2	$$⊢\phi \to B\in X$$
3	1	ersymb	$$⊢\phi \to \left(ARB\leftrightarrow BRA\right)$$
4	1 2	erth	$$⊢\phi \to \left(BRA\leftrightarrow \left[B\right]R=\left[A\right]R\right)$$
5		eqcom	$$⊢\left[B\right]R=\left[A\right]R\leftrightarrow \left[A\right]R=\left[B\right]R$$
6	4 5	bitrdi	$$⊢\phi \to \left(BRA\leftrightarrow \left[A\right]R=\left[B\right]R\right)$$
7	3 6	bitrd	$$⊢\phi \to \left(ARB\leftrightarrow \left[A\right]R=\left[B\right]R\right)$$