Theorem breqi

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

	Ref	Expression
Hypothesis	breqi.1	$$⊢R=S$$
Assertion	breqi	$$⊢ARB\leftrightarrow ASB$$

Proof

Step	Hyp	Ref	Expression
1		breqi.1	$$⊢R=S$$
2		breq	$$⊢R=S\to \left(ARB\leftrightarrow ASB\right)$$
3	1 2	ax-mp	$$⊢ARB\leftrightarrow ASB$$