Theorem eqbrrdiv

Description: Deduction from extensionality principle for relations. (Contributed by Rodolfo Medina, 10-Oct-2010)

	Ref	Expression
Hypotheses	eqbrrdiv.1	⊢ Rel 𝐴
	eqbrrdiv.2	⊢ Rel 𝐵
	eqbrrdiv.3	⊢ ( 𝜑 → ( 𝑥 𝐴 𝑦 ↔ 𝑥 𝐵 𝑦 ) )
Assertion	eqbrrdiv	⊢ ( 𝜑 → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eqbrrdiv.1	⊢ Rel 𝐴
2		eqbrrdiv.2	⊢ Rel 𝐵
3		eqbrrdiv.3	⊢ ( 𝜑 → ( 𝑥 𝐴 𝑦 ↔ 𝑥 𝐵 𝑦 ) )
4		df-br	⊢ ( 𝑥 𝐴 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
5		df-br	⊢ ( 𝑥 𝐵 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 )
6	3 4 5	3bitr3g	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
7	1 2 6	eqrelrdv	⊢ ( 𝜑 → 𝐴 = 𝐵 )