This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2reu5lem1

Description: Lemma for 2reu5 . Note that E! x e. A E! y e. B ph does not mean "there is exactly one x in A and exactly one y in B such that ph holds"; see comment for 2eu5 . (Contributed by Alexander van der Vekens, 17-Jun-2017)

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

Proof

Step	Hyp	Ref	Expression
1		df-reu	$⊢ \exists! y \in B φ \leftrightarrow \exists! y (y \in B \land φ)$
2	1	reubii	$⊢ \exists! x \in A \exists! y \in B φ \leftrightarrow \exists! x \in A \exists! y (y \in B \land φ)$
3		df-reu	$⊢ \exists! x \in A \exists! y (y \in B \land φ) \leftrightarrow \exists! x (x \in A \land \exists! y (y \in B \land φ))$
4		euanv	$⊢ \exists! y (x \in A \land (y \in B \land φ)) \leftrightarrow (x \in A \land \exists! y (y \in B \land φ))$
5	4	bicomi	$⊢ (x \in A \land \exists! y (y \in B \land φ)) \leftrightarrow \exists! y (x \in A \land (y \in B \land φ))$
6		3anass	$⊢ (x \in A \land y \in B \land φ) \leftrightarrow (x \in A \land (y \in B \land φ))$
7	6	bicomi	$⊢ (x \in A \land (y \in B \land φ)) \leftrightarrow (x \in A \land y \in B \land φ)$
8	7	eubii	$⊢ \exists! y (x \in A \land (y \in B \land φ)) \leftrightarrow \exists! y (x \in A \land y \in B \land φ)$
9	5 8	bitri	$⊢ (x \in A \land \exists! y (y \in B \land φ)) \leftrightarrow \exists! y (x \in A \land y \in B \land φ)$
10	9	eubii	$⊢ \exists! x (x \in A \land \exists! y (y \in B \land φ)) \leftrightarrow \exists! x \exists! y (x \in A \land y \in B \land φ)$
11	3 10	bitri	$⊢ \exists! x \in A \exists! y (y \in B \land φ) \leftrightarrow \exists! x \exists! y (x \in A \land y \in B \land φ)$
12	2 11	bitri	$⊢ \exists! x \in A \exists! y \in B φ \leftrightarrow \exists! x \exists! y (x \in A \land y \in B \land φ)$