2reu5lem2

		Ref	Expression
	Assertion	2reu5lem2	$⊢ \forall x \in A \exists^{} y \in B φ \leftrightarrow \forall x \exists^{} y (x \in A \land y \in B \land φ)$

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	bicomi	$⊢ (x \in A \to \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	mobii	$⊢ \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 \to \exists^{} y (y \in B \land φ)) \leftrightarrow \exists^{} y (x \in A \land y \in B \land φ)$
10	9	albii	$⊢ \forall x (x \in A \to \exists^{} y (y \in B \land φ)) \leftrightarrow \forall x \exists^{} y (x \in A \land y \in B \land φ)$
11	3 10	bitri	$⊢ \forall x \in A \exists^{} y (y \in B \land φ) \leftrightarrow \forall x \exists^{} y (x \in A \land y \in B \land φ)$
12	2 11	bitri	$⊢ \forall x \in A \exists^{} y \in B φ \leftrightarrow \forall x \exists^{} y (x \in A \land y \in B \land φ)$

Metamath Proof Explorer