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 CRACRB

Proof

Step Hyp Ref Expression
1 breq1i.1 A=B
2 breq2 A=BCRACRB
3 1 2 ax-mp CRACRB