Theorem eqrelriiv

Description: Inference from extensionality principle for relations. (Contributed by NM, 17-Mar-1995)

	Ref	Expression
Hypotheses	eqreliiv.1	$$⊢\mathrm{Rel}A$$
	eqreliiv.2	$$⊢\mathrm{Rel}B$$
	eqreliiv.3	$$⊢⟨x,y⟩\in A\leftrightarrow ⟨x,y⟩\in B$$
Assertion	eqrelriiv	$$⊢A=B$$

Proof

Step	Hyp	Ref	Expression
1		eqreliiv.1	$$⊢\mathrm{Rel}A$$
2		eqreliiv.2	$$⊢\mathrm{Rel}B$$
3		eqreliiv.3	$$⊢⟨x,y⟩\in A\leftrightarrow ⟨x,y⟩\in B$$
4	3	eqrelriv	$$⊢\left(\mathrm{Rel}A\wedge \mathrm{Rel}B\right)\to A=B$$
5	1 2 4	mp2an	$$⊢A=B$$