Metamath Proof Explorer

Theorem breq2i

Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996)

Ref Expression
Hypothesis breq1i.1 
|- A = B
Assertion breq2i 
|- ( C R A <-> C R B )

Proof

Step Hyp Ref Expression
1 breq1i.1 
 |-  A = B
2 breq2 
 |-  ( A = B -> ( C R A <-> C R B ) )
3 1 2 ax-mp 
 |-  ( C R A <-> C R B )