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

Metamath Proof Explorer

Theorem reeanv

Description: Rearrange restricted existential quantifiers. (Contributed by NM, 9-May-1999)

		Ref	Expression
	Assertion	reeanv	$⊢ \exists x \in A \exists y \in B (φ \land ψ) \leftrightarrow (\exists x \in A φ \land \exists y \in B ψ)$

Step	Hyp	Ref	Expression
1		exdistrv	$⊢ \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	1	reeanlem	$⊢ \exists x \in A \exists y \in B (φ \land ψ) \leftrightarrow (\exists x \in A φ \land \exists y \in B ψ)$