2reu2

Description: Double restricted existential uniqueness, analogous to 2eu2 . (Contributed by Alexander van der Vekens, 29-Jun-2017)

		Ref	Expression
	Assertion	2reu2	$⊢ \exists! y \in B \exists x \in A φ \to (\exists! x \in A \exists! y \in B φ \leftrightarrow \exists! x \in A \exists y \in B φ)$

Step	Hyp	Ref	Expression
1		reurmo	$⊢ \exists! y \in B \exists x \in A φ \to \exists^{*} y \in B \exists x \in A φ$
2		2rmorex	$⊢ \exists^{} y \in B \exists x \in A φ \to \forall x \in A \exists^{} y \in B φ$
3		2reu1	$⊢ \forall x \in A \exists^{*} y \in B φ \to (\exists! x \in A \exists! y \in B φ \leftrightarrow (\exists! x \in A \exists y \in B φ \land \exists! y \in B \exists x \in A φ))$
4		simpl	$⊢ (\exists! x \in A \exists y \in B φ \land \exists! y \in B \exists x \in A φ) \to \exists! x \in A \exists y \in B φ$
5	3 4	biimtrdi	$⊢ \forall x \in A \exists^{*} y \in B φ \to (\exists! x \in A \exists! y \in B φ \to \exists! x \in A \exists y \in B φ)$
6	1 2 5	3syl	$⊢ \exists! y \in B \exists x \in A φ \to (\exists! x \in A \exists! y \in B φ \to \exists! x \in A \exists y \in B φ)$
7		2rexreu	$⊢ (\exists! x \in A \exists y \in B φ \land \exists! y \in B \exists x \in A φ) \to \exists! x \in A \exists! y \in B φ$
8	7	expcom	$⊢ \exists! y \in B \exists x \in A φ \to (\exists! x \in A \exists y \in B φ \to \exists! x \in A \exists! y \in B φ)$
9	6 8	impbid	$⊢ \exists! y \in B \exists x \in A φ \to (\exists! x \in A \exists! y \in B φ \leftrightarrow \exists! x \in A \exists y \in B φ)$

Metamath Proof Explorer