2euex

Description: Double quantification with existential uniqueness. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker 2euexv when possible. (Contributed by NM, 3-Dec-2001) (Proof shortened by Andrew Salmon, 9-Jul-2011) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		df-eu	$⊢ \exists! x \exists y φ \leftrightarrow (\exists x \exists y φ \land \exists^{*} x \exists y φ)$
2		excom	$⊢ \exists x \exists y φ \leftrightarrow \exists y \exists x φ$
3		nfe1	$⊢ Ⅎ y \exists y φ$
4	3	nfmo	$⊢ Ⅎ y \exists^{*} x \exists y φ$
5		19.8a	$⊢ φ \to \exists y φ$
6	5	moimi	$⊢ \exists^{} x \exists y φ \to \exists^{} x φ$
7		moeu	$⊢ \exists^{*} x φ \leftrightarrow (\exists x φ \to \exists! x φ)$
8	6 7	sylib	$⊢ \exists^{*} x \exists y φ \to (\exists x φ \to \exists! x φ)$
9	4 8	eximd	$⊢ \exists^{*} x \exists y φ \to (\exists y \exists x φ \to \exists y \exists! x φ)$
10	2 9	biimtrid	$⊢ \exists^{*} x \exists y φ \to (\exists x \exists y φ \to \exists y \exists! x φ)$
11	10	impcom	$⊢ (\exists x \exists y φ \land \exists^{*} x \exists y φ) \to \exists y \exists! x φ$
12	1 11	sylbi	$⊢ \exists! x \exists y φ \to \exists y \exists! x φ$

Metamath Proof Explorer

Theorem 2euex

Proof