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 φ R Er X
erth2.2 φ B X
Assertion erth2 φ A R B A R = B R

Proof

Step Hyp Ref Expression
1 erth2.1 φ R Er X
2 erth2.2 φ B X
3 1 ersymb φ A R B B R A
4 1 2 erth φ B R A B R = A R
5 eqcom B R = A R A R = B R
6 4 5 bitrdi φ B R A A R = B R
7 3 6 bitrd φ A R B A R = B R