Theorem eqrelrdv

Description: Deduce equality of relations from equivalence of membership. (Contributed by Rodolfo Medina, 10-Oct-2010)

	Ref	Expression
Hypotheses	eqrelrdv.1	$$⊢\mathrm{Rel}A$$
	eqrelrdv.2	$$⊢\mathrm{Rel}B$$
	eqrelrdv.3	$$⊢\phi \to \left(⟨x,y⟩\in A\leftrightarrow ⟨x,y⟩\in B\right)$$
Assertion	eqrelrdv	$$⊢\phi \to A=B$$

Proof

Step	Hyp	Ref	Expression
1		eqrelrdv.1	$$⊢\mathrm{Rel}A$$
2		eqrelrdv.2	$$⊢\mathrm{Rel}B$$
3		eqrelrdv.3	$$⊢\phi \to \left(⟨x,y⟩\in A\leftrightarrow ⟨x,y⟩\in B\right)$$
4	3	alrimivv	$$⊢\phi \to \forall x\forall y\left(⟨x,y⟩\in A\leftrightarrow ⟨x,y⟩\in B\right)$$
5		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)$$
6	1 2 5	mp2an	$$⊢A=B\leftrightarrow \forall x\forall y\left(⟨x,y⟩\in A\leftrightarrow ⟨x,y⟩\in B\right)$$
7	4 6	sylibr	$$⊢\phi \to A=B$$