This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2eu2ex

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

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

Step	Hyp	Ref	Expression
1		euex	$⊢ \exists! x \exists! y φ \to \exists x \exists! y φ$
2		euex	$⊢ \exists! y φ \to \exists y φ$
3	2	eximi	$⊢ \exists x \exists! y φ \to \exists x \exists y φ$
4	1 3	syl	$⊢ \exists! x \exists! y φ \to \exists x \exists y φ$