2reuswap

Description: A condition allowing swap of uniqueness and existential quantifiers. (Contributed by Thierry Arnoux, 7-Apr-2017) (Revised by NM, 16-Jun-2017)

		Ref	Expression
	Assertion	2reuswap	$⊢ \forall 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 φ)$

Proof

Step	Hyp	Ref	Expression
1		df-rmo	$⊢ \exists^{} y \in B φ \leftrightarrow \exists^{} y (y \in B \land φ)$
2	1	ralbii	$⊢ \forall x \in A \exists^{} y \in B φ \leftrightarrow \forall x \in A \exists^{} y (y \in B \land φ)$
3		df-ral	$⊢ \forall x \in A \exists^{} y (y \in B \land φ) \leftrightarrow \forall x (x \in A \to \exists^{} y (y \in B \land φ))$
4		moanimv	$⊢ \exists^{} y (x \in A \land (y \in B \land φ)) \leftrightarrow (x \in A \to \exists^{} y (y \in B \land φ))$
5	4	albii	$⊢ \forall x \exists^{} y (x \in A \land (y \in B \land φ)) \leftrightarrow \forall x (x \in A \to \exists^{} y (y \in B \land φ))$
6	3 5	bitr4i	$⊢ \forall x \in A \exists^{} y (y \in B \land φ) \leftrightarrow \forall x \exists^{} y (x \in A \land (y \in B \land φ))$
7		2euswapv	$⊢ \forall x \exists^{*} y (x \in A \land (y \in B \land φ)) \to (\exists! x \exists y (x \in A \land (y \in B \land φ)) \to \exists! y \exists x (x \in A \land (y \in B \land φ)))$
8		df-reu	$⊢ \exists! x \in A \exists y \in B φ \leftrightarrow \exists! x (x \in A \land \exists y \in B φ)$
9		r19.42v	$⊢ \exists y \in B (x \in A \land φ) \leftrightarrow (x \in A \land \exists y \in B φ)$
10		df-rex	$⊢ \exists y \in B (x \in A \land φ) \leftrightarrow \exists y (y \in B \land (x \in A \land φ))$
11	9 10	bitr3i	$⊢ (x \in A \land \exists y \in B φ) \leftrightarrow \exists y (y \in B \land (x \in A \land φ))$
12		an12	$⊢ (y \in B \land (x \in A \land φ)) \leftrightarrow (x \in A \land (y \in B \land φ))$
13	12	exbii	$⊢ \exists y (y \in B \land (x \in A \land φ)) \leftrightarrow \exists y (x \in A \land (y \in B \land φ))$
14	11 13	bitri	$⊢ (x \in A \land \exists y \in B φ) \leftrightarrow \exists y (x \in A \land (y \in B \land φ))$
15	14	eubii	$⊢ \exists! x (x \in A \land \exists y \in B φ) \leftrightarrow \exists! x \exists y (x \in A \land (y \in B \land φ))$
16	8 15	bitri	$⊢ \exists! x \in A \exists y \in B φ \leftrightarrow \exists! x \exists y (x \in A \land (y \in B \land φ))$
17		df-reu	$⊢ \exists! y \in B \exists x \in A φ \leftrightarrow \exists! y (y \in B \land \exists x \in A φ)$
18		r19.42v	$⊢ \exists x \in A (y \in B \land φ) \leftrightarrow (y \in B \land \exists x \in A φ)$
19		df-rex	$⊢ \exists x \in A (y \in B \land φ) \leftrightarrow \exists x (x \in A \land (y \in B \land φ))$
20	18 19	bitr3i	$⊢ (y \in B \land \exists x \in A φ) \leftrightarrow \exists x (x \in A \land (y \in B \land φ))$
21	20	eubii	$⊢ \exists! y (y \in B \land \exists x \in A φ) \leftrightarrow \exists! y \exists x (x \in A \land (y \in B \land φ))$
22	17 21	bitri	$⊢ \exists! y \in B \exists x \in A φ \leftrightarrow \exists! y \exists x (x \in A \land (y \in B \land φ))$
23	7 16 22	3imtr4g	$⊢ \forall x \exists^{*} y (x \in A \land (y \in B \land φ)) \to (\exists! x \in A \exists y \in B φ \to \exists! y \in B \exists x \in A φ)$
24	6 23	sylbi	$⊢ \forall x \in A \exists^{*} y (y \in B \land φ) \to (\exists! x \in A \exists y \in B φ \to \exists! y \in B \exists x \in A φ)$
25	2 24	sylbi	$⊢ \forall 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 φ)$

Metamath Proof Explorer

Theorem 2reuswap

Proof