Metamath Proof Explorer

Theorem breq

Description: Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995)

Ref Expression
Assertion breq 
|- ( R = S -> ( A R B <-> A S B ) )

Proof

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