Theorem 2eu2ex

Description: Double existential uniqueness. (Contributed by NM, 3-Dec-2001)

	Ref	Expression
Assertion	2eu2ex	$$⊢\exists !x\exists !y\phi \to \exists x\exists y\phi$$

Proof

Step	Hyp	Ref	Expression
1		euex	$$⊢\exists !x\exists !y\phi \to \exists x\exists !y\phi$$
2		euex	$$⊢\exists !y\phi \to \exists y\phi$$
3	2	eximi	$$⊢\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$$