Theorem 2exeuv

Description: Double existential uniqueness implies double unique existential quantification. Version of 2exeu with x and y distinct, but not requiring ax-13 . (Contributed by NM, 3-Dec-2001) (Revised by Wolf Lammen, 2-Oct-2023)

	Ref	Expression
Assertion	2exeuv	$$⊢\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\to \exists !x\exists !y\phi$$

Proof

Step	Hyp	Ref	Expression
1		eumo	$$⊢\exists !x\exists y\phi \to {\exists }^{*}x\exists y\phi$$
2		euex	$$⊢\exists !y\phi \to \exists y\phi$$
3	2	moimi	$$⊢{\exists }^{*}x\exists y\phi \to {\exists }^{*}x\exists !y\phi$$
4	1 3	syl	$$⊢\exists !x\exists y\phi \to {\exists }^{*}x\exists !y\phi$$
5		2euexv	$$⊢\exists !y\exists x\phi \to \exists x\exists !y\phi$$
6	4 5	anim12ci	$$⊢\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\to \left(\exists x\exists !y\phi \wedge {\exists }^{*}x\exists !y\phi \right)$$
7		df-eu	$$⊢\exists !x\exists !y\phi \leftrightarrow \left(\exists x\exists !y\phi \wedge {\exists }^{*}x\exists !y\phi \right)$$
8	6 7	sylibr	$$⊢\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\to \exists !x\exists !y\phi$$