Theorem breq2

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

	Ref	Expression
Assertion	breq2	⊢ ( 𝐴 = 𝐵 → ( 𝐶 𝑅 𝐴 ↔ 𝐶 𝑅 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		opeq2	⊢ ( 𝐴 = 𝐵 → ⟨ 𝐶 , 𝐴 ⟩ = ⟨ 𝐶 , 𝐵 ⟩ )
2	1	eleq1d	⊢ ( 𝐴 = 𝐵 → ( ⟨ 𝐶 , 𝐴 ⟩ ∈ 𝑅 ↔ ⟨ 𝐶 , 𝐵 ⟩ ∈ 𝑅 ) )
3		df-br	⊢ ( 𝐶 𝑅 𝐴 ↔ ⟨ 𝐶 , 𝐴 ⟩ ∈ 𝑅 )
4		df-br	⊢ ( 𝐶 𝑅 𝐵 ↔ ⟨ 𝐶 , 𝐵 ⟩ ∈ 𝑅 )
5	2 3 4	3bitr4g	⊢ ( 𝐴 = 𝐵 → ( 𝐶 𝑅 𝐴 ↔ 𝐶 𝑅 𝐵 ) )