# Metamath Proof Explorer

## 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({A}{R}{B}↔\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({A}{R}{B}↔{B}{R}{A}\right)$
4 1 2 erth ${⊢}{\phi }\to \left({B}{R}{A}↔\left[{B}\right]{R}=\left[{A}\right]{R}\right)$
5 eqcom ${⊢}\left[{B}\right]{R}=\left[{A}\right]{R}↔\left[{A}\right]{R}=\left[{B}\right]{R}$
6 4 5 syl6bb ${⊢}{\phi }\to \left({B}{R}{A}↔\left[{A}\right]{R}=\left[{B}\right]{R}\right)$
7 3 6 bitrd ${⊢}{\phi }\to \left({A}{R}{B}↔\left[{A}\right]{R}=\left[{B}\right]{R}\right)$