Description: Rearrange restricted existential quantifiers. (Contributed by NM, 9-May-1999)
Ref | Expression | ||
---|---|---|---|
Assertion | reeanv | ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑦 ∈ 𝐵 𝜓 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exdistrv | ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) ) ) | |
2 | 1 | reeanlem | ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑦 ∈ 𝐵 𝜓 ) ) |