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

Metamath Proof Explorer

Theorem breq1

Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993)

Ref Expression
Assertion breq1 ⊢ A = B → A R C ↔ B R C

Proof

Step Hyp Ref Expression
1 opeq1 ⊢ A = B → A C = B C
2 1 eleq1d ⊢ A = B → A C ∈ R ↔ B C ∈ R
3 df-br ⊢ A R C ↔ A C ∈ R
4 df-br ⊢ B R C ↔ B C ∈ R
5 2 3 4 3bitr4g ⊢ A = B → A R C ↔ B R C