Theorem 2exeu

Description: Double existential uniqueness implies double unique existential quantification. The converse does not hold. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker 2exeuv when possible. (Contributed by NM, 3-Dec-2001) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

	Ref	Expression
Assertion	2exeu	$$⊢\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		2euex	$$⊢\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$$