Theorem eqrelriiv

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

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

Proof

Step	Hyp	Ref	Expression
1		eqrelriiv.1	$$⊢\mathrm{Rel}A$$
2		eqrelriiv.2	$$⊢\mathrm{Rel}B$$
3		eqrelriiv.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$$