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

Metamath Proof Explorer

Theorem breq

Description: Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995)

		Ref	Expression
	Assertion	breq	$⊢ R = S \to (A R B \leftrightarrow A S B)$

Step	Hyp	Ref	Expression
1		eleq2	$⊢ R = S \to (⟨A, B⟩ \in R \leftrightarrow ⟨A, B⟩ \in S)$
2		df-br	$⊢ A R B \leftrightarrow ⟨A, B⟩ \in R$
3		df-br	$⊢ A S B \leftrightarrow ⟨A, B⟩ \in S$
4	1 2 3	3bitr4g	$⊢ R = S \to (A R B \leftrightarrow A S B)$