Theorem 2reu2

Description: Double restricted existential uniqueness, analogous to 2eu2 . (Contributed by Alexander van der Vekens, 29-Jun-2017)

	Ref	Expression
Assertion	2reu2	$$⊢\exists !y\in B\exists x\in A\phi \to \left(\exists !x\in A\exists !y\in B\phi \leftrightarrow \exists !x\in A\exists y\in B\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		reurmo	$$⊢\exists !y\in B\exists x\in A\phi \to {\exists }^{*}y\in B\exists x\in A\phi$$
2		2rmorex	$$⊢{\exists }^{*}y\in B\exists x\in A\phi \to \forall x\in A{\exists }^{*}y\in B\phi$$
3		2reu1	$$⊢\forall x\in A{\exists }^{*}y\in B\phi \to \left(\exists !x\in A\exists !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)$$
4		simpl	$$⊢\left(\exists !x\in A\exists y\in B\phi \wedge \exists !y\in B\exists x\in A\phi \right)\to \exists !x\in A\exists y\in B\phi$$
5	3 4	biimtrdi	$$⊢\forall x\in A{\exists }^{*}y\in B\phi \to \left(\exists !x\in A\exists !y\in B\phi \to \exists !x\in A\exists y\in B\phi \right)$$
6	1 2 5	3syl	$$⊢\exists !y\in B\exists x\in A\phi \to \left(\exists !x\in A\exists !y\in B\phi \to \exists !x\in A\exists y\in B\phi \right)$$
7		2rexreu	$$⊢\left(\exists !x\in A\exists y\in B\phi \wedge \exists !y\in B\exists x\in A\phi \right)\to \exists !x\in A\exists !y\in B\phi$$
8	7	expcom	$$⊢\exists !y\in B\exists x\in A\phi \to \left(\exists !x\in A\exists y\in B\phi \to \exists !x\in A\exists !y\in B\phi \right)$$
9	6 8	impbid	$$⊢\exists !y\in B\exists x\in A\phi \to \left(\exists !x\in A\exists !y\in B\phi \leftrightarrow \exists !x\in A\exists y\in B\phi \right)$$