reeanlem

Description: Lemma factoring out common proof steps of reeanv and reean . (Contributed by Wolf Lammen, 20-Aug-2023)

		Ref	Expression
	Hypothesis	reeanlem.1	$⊢ \exists x \exists y ((x \in A \land φ) \land (y \in B \land ψ)) \leftrightarrow (\exists x (x \in A \land φ) \land \exists y (y \in B \land ψ))$
	Assertion	reeanlem	$⊢ \exists x \in A \exists y \in B (φ \land ψ) \leftrightarrow (\exists x \in A φ \land \exists y \in B ψ)$

Step	Hyp	Ref	Expression
1		reeanlem.1	$⊢ \exists x \exists y ((x \in A \land φ) \land (y \in B \land ψ)) \leftrightarrow (\exists x (x \in A \land φ) \land \exists y (y \in B \land ψ))$
2		an4	$⊢ ((x \in A \land y \in B) \land (φ \land ψ)) \leftrightarrow ((x \in A \land φ) \land (y \in B \land ψ))$
3	2	2exbii	$⊢ \exists x \exists y ((x \in A \land y \in B) \land (φ \land ψ)) \leftrightarrow \exists x \exists y ((x \in A \land φ) \land (y \in B \land ψ))$
4	3 1	bitri	$⊢ \exists x \exists y ((x \in A \land y \in B) \land (φ \land ψ)) \leftrightarrow (\exists x (x \in A \land φ) \land \exists y (y \in B \land ψ))$
5		r2ex	$⊢ \exists x \in A \exists y \in B (φ \land ψ) \leftrightarrow \exists x \exists y ((x \in A \land y \in B) \land (φ \land ψ))$
6		df-rex	$⊢ \exists x \in A φ \leftrightarrow \exists x (x \in A \land φ)$
7		df-rex	$⊢ \exists y \in B ψ \leftrightarrow \exists y (y \in B \land ψ)$
8	6 7	anbi12i	$⊢ (\exists x \in A φ \land \exists y \in B ψ) \leftrightarrow (\exists x (x \in A \land φ) \land \exists y (y \in B \land ψ))$
9	4 5 8	3bitr4i	$⊢ \exists x \in A \exists y \in B (φ \land ψ) \leftrightarrow (\exists x \in A φ \land \exists y \in B ψ)$

Metamath Proof Explorer