Description: Distribute existential quantifiers. (Contributed by NM, 27-Oct-2010) (Revised by Mario Carneiro, 6-Oct-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | eean.1 | ⊢ Ⅎ 𝑦 𝜑 | |
eean.2 | ⊢ Ⅎ 𝑥 𝜓 | ||
Assertion | eean | ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜓 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eean.1 | ⊢ Ⅎ 𝑦 𝜑 | |
2 | eean.2 | ⊢ Ⅎ 𝑥 𝜓 | |
3 | 1 | 19.42 | ⊢ ( ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∃ 𝑦 𝜓 ) ) |
4 | 3 | exbii | ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑥 ( 𝜑 ∧ ∃ 𝑦 𝜓 ) ) |
5 | 2 | nfex | ⊢ Ⅎ 𝑥 ∃ 𝑦 𝜓 |
6 | 5 | 19.41 | ⊢ ( ∃ 𝑥 ( 𝜑 ∧ ∃ 𝑦 𝜓 ) ↔ ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜓 ) ) |
7 | 4 6 | bitri | ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜓 ) ) |