Theorem eqrelrdv2

Description: A version of eqrelrdv . (Contributed by Rodolfo Medina, 10-Oct-2010)

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

Proof

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