Description: Equality theorem for a binary relation. (Contributed by NM, 31Dec1993)
Ref  Expression  

Assertion  breq1   ( A = B > ( A R C <> B R C ) ) 
Step  Hyp  Ref  Expression 

1  opeq1   ( A = B > <. A , C >. = <. B , C >. ) 

2  1  eleq1d   ( A = B > ( <. A , C >. e. R <> <. B , C >. e. R ) ) 
3  dfbr   ( A R C <> <. A , C >. e. R ) 

4  dfbr   ( B R C <> <. B , C >. e. R ) 

5  2 3 4  3bitr4g   ( A = B > ( A R C <> B R C ) ) 