Metamath Proof Explorer

Theorem breq2

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

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

Proof

Step Hyp Ref Expression
1 opeq2 
 |-  ( A = B -> <. C , A >. = <. C , B >. )
2 1 eleq1d 
 |-  ( A = B -> ( <. C , A >. e. R <-> <. C , B >. e. R ) )
3 df-br 
 |-  ( C R A <-> <. C , A >. e. R )
4 df-br 
 |-  ( C R B <-> <. C , B >. e. R )
5 2 3 4 3bitr4g 
 |-  ( A = B -> ( C R A <-> C R B ) )