Metamath Proof Explorer

Theorem 2reurex

Description: Double restricted quantification with existential uniqueness, analogous to 2euex . (Contributed by Alexander van der Vekens, 24-Jun-2017)

		Ref	Expression
	Assertion	2reurex	$⊢ \exists! x \in A \exists y \in B φ \to \exists y \in B \exists! x \in A φ$

Proof

Step	Hyp	Ref	Expression
1		reu5	$⊢ \exists! x \in A \exists y \in B φ \leftrightarrow (\exists x \in A \exists y \in B φ \land \exists^{*} x \in A \exists y \in B φ)$
2		rexcom	$⊢ \exists x \in A \exists y \in B φ \leftrightarrow \exists y \in B \exists x \in A φ$
3		nfcv	$⊢ \underline{Ⅎ} y A$
4		nfre1	$⊢ Ⅎ y \exists y \in B φ$
5	3 4	nfrmow	$⊢ Ⅎ y \exists^{*} x \in A \exists y \in B φ$
6		rspe	$⊢ (y \in B \land φ) \to \exists y \in B φ$
7	6	ex	$⊢ y \in B \to (φ \to \exists y \in B φ)$
8	7	ralrimivw	$⊢ y \in B \to \forall x \in A (φ \to \exists y \in B φ)$
9		rmoim	$⊢ \forall x \in A (φ \to \exists y \in B φ) \to (\exists^{} x \in A \exists y \in B φ \to \exists^{} x \in A φ)$
10	8 9	syl	$⊢ y \in B \to (\exists^{} x \in A \exists y \in B φ \to \exists^{} x \in A φ)$
11	10	impcom	$⊢ (\exists^{} x \in A \exists y \in B φ \land y \in B) \to \exists^{} x \in A φ$
12		rmo5	$⊢ \exists^{*} x \in A φ \leftrightarrow (\exists x \in A φ \to \exists! x \in A φ)$
13	11 12	sylib	$⊢ (\exists^{*} x \in A \exists y \in B φ \land y \in B) \to (\exists x \in A φ \to \exists! x \in A φ)$
14	13	ex	$⊢ \exists^{*} x \in A \exists y \in B φ \to (y \in B \to (\exists x \in A φ \to \exists! x \in A φ))$
15	5 14	reximdai	$⊢ \exists^{*} x \in A \exists y \in B φ \to (\exists y \in B \exists x \in A φ \to \exists y \in B \exists! x \in A φ)$
16	2 15	syl5bi	$⊢ \exists^{*} x \in A \exists y \in B φ \to (\exists x \in A \exists y \in B φ \to \exists y \in B \exists! x \in A φ)$
17	16	impcom	$⊢ (\exists x \in A \exists y \in B φ \land \exists^{*} x \in A \exists y \in B φ) \to \exists y \in B \exists! x \in A φ$
18	1 17	sylbi	$⊢ \exists! x \in A \exists y \in B φ \to \exists y \in B \exists! x \in A φ$