Metamath Proof Explorer

Theorem reean

Description: Rearrange restricted existential quantifiers. For a version based on fewer axioms see reeanv . (Contributed by NM, 27-Oct-2010) (Proof shortened by Andrew Salmon, 30-May-2011)

		Ref	Expression
	Hypotheses	reean.1	$⊢ Ⅎ y φ$
		reean.2	$⊢ Ⅎ x ψ$
	Assertion	reean	$⊢ \exists x \in A \exists y \in B (φ \land ψ) \leftrightarrow (\exists x \in A φ \land \exists y \in B ψ)$

Proof

Step	Hyp	Ref	Expression
1		reean.1	$⊢ Ⅎ y φ$
2		reean.2	$⊢ Ⅎ x ψ$
3		nfv	$⊢ Ⅎ y x \in A$
4	3 1	nfan	$⊢ Ⅎ y (x \in A \land φ)$
5		nfv	$⊢ Ⅎ x y \in B$
6	5 2	nfan	$⊢ Ⅎ x (y \in B \land ψ)$
7	4 6	eean	$⊢ \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 ψ))$
8	7	reeanlem	$⊢ \exists x \in A \exists y \in B (φ \land ψ) \leftrightarrow (\exists x \in A φ \land \exists y \in B ψ)$