2reuswap2

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

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

Proof

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

Metamath Proof Explorer

Theorem 2reuswap2

Proof