eean

Description: Distribute existential quantifiers. (Contributed by NM, 27-Oct-2010) (Revised by Mario Carneiro, 6-Oct-2016)

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

Step	Hyp	Ref	Expression
1		eean.1	$⊢ Ⅎ y φ$
2		eean.2	$⊢ Ⅎ x ψ$
3	1	19.42	$⊢ \exists y (φ \land ψ) \leftrightarrow (φ \land \exists y ψ)$
4	3	exbii	$⊢ \exists x \exists y (φ \land ψ) \leftrightarrow \exists x (φ \land \exists y ψ)$
5	2	nfex	$⊢ Ⅎ x \exists y ψ$
6	5	19.41	$⊢ \exists x (φ \land \exists y ψ) \leftrightarrow (\exists x φ \land \exists y ψ)$
7	4 6	bitri	$⊢ \exists x \exists y (φ \land ψ) \leftrightarrow (\exists x φ \land \exists y ψ)$

Metamath Proof Explorer