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

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 ⊢ Ⅎ 𝑦 𝜑
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 ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑦 ∈ 𝐵 𝜓 ) )