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, 30Jul1995) (Revised by Mario Carneiro, 6Jul2015)
Ref  Expression  

Hypotheses  erth2.1   ( ph > R Er X ) 

erth2.2   ( ph > B e. X ) 

Assertion  erth2   ( ph > ( A R B <> [ A ] R = [ B ] R ) ) 
Step  Hyp  Ref  Expression 

1  erth2.1   ( ph > R Er X ) 

2  erth2.2   ( ph > B e. X ) 

3  1  ersymb   ( ph > ( A R B <> B R A ) ) 
4  1 2  erth   ( ph > ( B R A <> [ B ] R = [ A ] R ) ) 
5  eqcom   ( [ B ] R = [ A ] R <> [ A ] R = [ B ] R ) 

6  4 5  syl6bb   ( ph > ( B R A <> [ A ] R = [ B ] R ) ) 
7  3 6  bitrd   ( ph > ( A R B <> [ A ] R = [ B ] R ) ) 