Theorem breqi

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

	Ref	Expression
Hypothesis	breqi.1	⊢ 𝑅 = 𝑆
Assertion	breqi	⊢ ( 𝐴 𝑅 𝐵 ↔ 𝐴 𝑆 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		breqi.1	⊢ 𝑅 = 𝑆
2		breq	⊢ ( 𝑅 = 𝑆 → ( 𝐴 𝑅 𝐵 ↔ 𝐴 𝑆 𝐵 ) )
3	1 2	ax-mp	⊢ ( 𝐴 𝑅 𝐵 ↔ 𝐴 𝑆 𝐵 )