Metamath Proof Explorer

Theorem breq1

Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993)

Ref Expression
Assertion breq1 
|- ( A = B -> ( A R C <-> B R C ) )

Proof

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 df-br 
 |-  ( A R C <-> <. A , C >. e. R )
4 df-br 
 |-  ( B R C <-> <. B , C >. e. R )
5 2 3 4 3bitr4g 
 |-  ( A = B -> ( A R C <-> B R C ) )