Metamath Proof Explorer

Theorem breq1i

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

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

Proof

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