This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem breqi

Description: Equality inference for binary relations. (Contributed by NM, 19-Feb-2005)

Ref Expression
Hypothesis breqi.1 ⊢ R = S
Assertion breqi ⊢ A R B ↔ A S B

Proof

Step Hyp Ref Expression
1 breqi.1 ⊢ R = S
2 breq ⊢ R = S → A R B ↔ A S B
3 1 2 ax-mp ⊢ A R B ↔ A S B