Theorem eqrelriv

Description: Inference from extensionality principle for relations. (Contributed by FL, 15-Oct-2012)

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

Proof

Step	Hyp	Ref	Expression
1		eqrelriv.1	$$⊢⟨x,y⟩\in A\leftrightarrow ⟨x,y⟩\in B$$
2	1	gen2	$$⊢\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	mpbiri	$$⊢\left(\mathrm{Rel}A\wedge \mathrm{Rel}B\right)\to A=B$$