Description: Basic property of equivalence relations. Part of Lemma 3N of Enderton p. 57. (Contributed by NM, 30Jul1995) (Revised by Mario Carneiro, 9Jul2014)
Ref  Expression  

Hypotheses  erthi.1   ( ph > R Er X ) 

erthi.2   ( ph > A R B ) 

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

1  erthi.1   ( ph > R Er X ) 

2  erthi.2   ( ph > A R B ) 

3  1 2  ercl   ( ph > A e. X ) 
4  1 3  erth   ( ph > ( A R B <> [ A ] R = [ B ] R ) ) 
5  2 4  mpbid   ( ph > [ A ] R = [ B ] R ) 