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

Metamath Proof Explorer

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	$⊢ (\exists! x \exists y φ \land \exists! y \exists x φ) \to \exists! x \exists! y φ$

Proof

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