Theorem eqbrrdva

Description: Deduction from extensionality principle for relations, given an equivalence only on the relation domain and range. (Contributed by Thierry Arnoux, 28-Nov-2017)

	Ref	Expression
Hypotheses	eqbrrdva.1	$$⊢\phi \to A\subseteq C\times D$$
	eqbrrdva.2	$$⊢\phi \to B\subseteq C\times D$$
	eqbrrdva.3	$$⊢\left(\phi \wedge x\in C\wedge y\in D\right)\to \left(xAy\leftrightarrow xBy\right)$$
Assertion	eqbrrdva	$$⊢\phi \to A=B$$

Proof

Step	Hyp	Ref	Expression
1		eqbrrdva.1	$$⊢\phi \to A\subseteq C\times D$$
2		eqbrrdva.2	$$⊢\phi \to B\subseteq C\times D$$
3		eqbrrdva.3	$$⊢\left(\phi \wedge x\in C\wedge y\in D\right)\to \left(xAy\leftrightarrow xBy\right)$$
4		xpss	$$⊢C\times D\subseteq \mathrm{V}\times \mathrm{V}$$
5	1 4	sstrdi	$$⊢\phi \to A\subseteq \mathrm{V}\times \mathrm{V}$$
6		df-rel	$$⊢\mathrm{Rel}A\leftrightarrow A\subseteq \mathrm{V}\times \mathrm{V}$$
7	5 6	sylibr	$$⊢\phi \to \mathrm{Rel}A$$
8	2 4	sstrdi	$$⊢\phi \to B\subseteq \mathrm{V}\times \mathrm{V}$$
9		df-rel	$$⊢\mathrm{Rel}B\leftrightarrow B\subseteq \mathrm{V}\times \mathrm{V}$$
10	8 9	sylibr	$$⊢\phi \to \mathrm{Rel}B$$
11	1	ssbrd	$$⊢\phi \to \left(xAy\to x\left(C\times D\right)y\right)$$
12		brxp	$$⊢x\left(C\times D\right)y\leftrightarrow \left(x\in C\wedge y\in D\right)$$
13	11 12	syl6ib	$$⊢\phi \to \left(xAy\to \left(x\in C\wedge y\in D\right)\right)$$
14	2	ssbrd	$$⊢\phi \to \left(xBy\to x\left(C\times D\right)y\right)$$
15	14 12	syl6ib	$$⊢\phi \to \left(xBy\to \left(x\in C\wedge y\in D\right)\right)$$
16	3	3expib	$$⊢\phi \to \left(\left(x\in C\wedge y\in D\right)\to \left(xAy\leftrightarrow xBy\right)\right)$$
17	13 15 16	pm5.21ndd	$$⊢\phi \to \left(xAy\leftrightarrow xBy\right)$$
18	7 10 17	eqbrrdv	$$⊢\phi \to A=B$$