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 ⊢ ∃ x ∈ A ∃ y ∈ B φ ∧ ψ ↔ ∃ x ∈ A φ ∧ ∃ y ∈ B ψ

Proof

Step Hyp Ref Expression
1 reean.1 ⊢ Ⅎ y φ
2 reean.2 ⊢ Ⅎ x ψ
3 nfv ⊢ Ⅎ y x ∈ A
4 3 1 nfan ⊢ Ⅎ y x ∈ A ∧ φ
5 nfv ⊢ Ⅎ x y ∈ B
6 5 2 nfan ⊢ Ⅎ x y ∈ B ∧ ψ
7 4 6 eean ⊢ ∃ x ∃ y x ∈ A ∧ φ ∧ y ∈ B ∧ ψ ↔ ∃ x x ∈ A ∧ φ ∧ ∃ y y ∈ B ∧ ψ
8 7 reeanlem ⊢ ∃ x ∈ A ∃ y ∈ B φ ∧ ψ ↔ ∃ x ∈ A φ ∧ ∃ y ∈ B ψ