Theorem breq

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

	Ref	Expression
Assertion	breq	$$⊢R=S\to \left(ARB\leftrightarrow ASB\right)$$

Proof

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