Theorem reean

Description: Rearrange restricted existential quantifiers. (Contributed by NM, 27-Oct-2010) (Proof shortened by Andrew Salmon, 30-May-2011)

	Ref	Expression
Hypotheses	reean.1	⊢ Ⅎ 𝑦 𝜑
	reean.2	⊢ Ⅎ 𝑥 𝜓
Assertion	reean	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑦 ∈ 𝐵 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		reean.1	⊢ Ⅎ 𝑦 𝜑
2		reean.2	⊢ Ⅎ 𝑥 𝜓
3		nfv	⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
4	3 1	nfan	⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
5		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐵
6	5 2	nfan	⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐵 ∧ 𝜓 )
7	4 6	eean	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) ) )
8	7	reeanlem	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑦 ∈ 𝐵 𝜓 ) )