Theorem eqbrrdiv

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

	Ref	Expression
Hypotheses	eqbrrdiv.1	$$⊢\mathrm{Rel}A$$
	eqbrrdiv.2	$$⊢\mathrm{Rel}B$$
	eqbrrdiv.3	$$⊢\phi \to \left(xAy\leftrightarrow xBy\right)$$
Assertion	eqbrrdiv	$$⊢\phi \to A=B$$

Proof

Step	Hyp	Ref	Expression
1		eqbrrdiv.1	$$⊢\mathrm{Rel}A$$
2		eqbrrdiv.2	$$⊢\mathrm{Rel}B$$
3		eqbrrdiv.3	$$⊢\phi \to \left(xAy\leftrightarrow xBy\right)$$
4		df-br	$$⊢xAy\leftrightarrow ⟨x,y⟩\in A$$
5		df-br	$$⊢xBy\leftrightarrow ⟨x,y⟩\in B$$
6	3 4 5	3bitr3g	$$⊢\phi \to \left(⟨x,y⟩\in A\leftrightarrow ⟨x,y⟩\in B\right)$$
7	1 2 6	eqrelrdv	$$⊢\phi \to A=B$$