Theorem eqbrrdv

Description: Deduction from extensionality principle for relations. (Contributed by Mario Carneiro, 3-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		eqbrrdv.1	$$⊢\phi \to \mathrm{Rel}A$$
2		eqbrrdv.2	$$⊢\phi \to \mathrm{Rel}B$$
3		eqbrrdv.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	6	alrimivv	$$⊢\phi \to \forall x\forall y\left(⟨x,y⟩\in A\leftrightarrow ⟨x,y⟩\in B\right)$$
8		eqrel	$$⊢\left(\mathrm{Rel}A\wedge \mathrm{Rel}B\right)\to \left(A=B\leftrightarrow \forall x\forall y\left(⟨x,y⟩\in A\leftrightarrow ⟨x,y⟩\in B\right)\right)$$
9	1 2 8	syl2anc	$$⊢\phi \to \left(A=B\leftrightarrow \forall x\forall y\left(⟨x,y⟩\in A\leftrightarrow ⟨x,y⟩\in B\right)\right)$$
10	7 9	mpbird	$$⊢\phi \to A=B$$