Definition df-2reu

Description: Define the double restricted existential uniqueness quantifier. (Contributed by Thierry Arnoux, 4-Jul-2023)

	Ref	Expression
Assertion	df-2reu	$$⊢\exists !x\in A,y\in B\phi \leftrightarrow \left(\exists !x\in A\exists y\in B\phi \wedge \exists !y\in B\exists x\in A\phi \right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2		vy	$$setvary$$
3		cB	$$classB$$
4		wph	$$wff\phi$$
5	4 0 2 1 3	w2reu	$$wff\exists !x\in A,y\in B\phi$$
6	4 2 3	wrex	$$wff\exists y\in B\phi$$
7	6 0 1	wreu	$$wff\exists !x\in A\exists y\in B\phi$$
8	4 0 1	wrex	$$wff\exists x\in A\phi$$
9	8 2 3	wreu	$$wff\exists !y\in B\exists x\in A\phi$$
10	7 9	wa	$$wff\left(\exists !x\in A\exists y\in B\phi \wedge \exists !y\in B\exists x\in A\phi \right)$$
11	5 10	wb	$$wff\left(\exists !x\in A,y\in B\phi \leftrightarrow \left(\exists !x\in A\exists y\in B\phi \wedge \exists !y\in B\exists x\in A\phi \right)\right)$$