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

Metamath Proof Explorer

Theorem eeor

Description: Distribute existential quantifiers. (Contributed by NM, 8-Aug-1994) Avoid ax-10 . (Revised by GG, 21-Nov-2024)

Ref Expression
Hypotheses eeor.1 ⊢ Ⅎ y φ
eeor.2 ⊢ Ⅎ x ψ
Assertion eeor ⊢ ∃ x ∃ y φ ∨ ψ ↔ ∃ x φ ∨ ∃ y ψ

Proof

Step Hyp Ref Expression
1 eeor.1 ⊢ Ⅎ y φ
2 eeor.2 ⊢ Ⅎ x ψ
3 19.43 ⊢ ∃ y φ ∨ ψ ↔ ∃ y φ ∨ ∃ y ψ
4 3 exbii ⊢ ∃ x ∃ y φ ∨ ψ ↔ ∃ x ∃ y φ ∨ ∃ y ψ
5 19.43 ⊢ ∃ x ∃ y φ ∨ ∃ y ψ ↔ ∃ x ∃ y φ ∨ ∃ x ∃ y ψ
6 1 19.9 ⊢ ∃ y φ ↔ φ
7 6 exbii ⊢ ∃ x ∃ y φ ↔ ∃ x φ
8 excom ⊢ ∃ x ∃ y ψ ↔ ∃ y ∃ x ψ
9 2 19.9 ⊢ ∃ x ψ ↔ ψ
10 9 exbii ⊢ ∃ y ∃ x ψ ↔ ∃ y ψ
11 8 10 bitri ⊢ ∃ x ∃ y ψ ↔ ∃ y ψ
12 7 11 orbi12i ⊢ ∃ x ∃ y φ ∨ ∃ x ∃ y ψ ↔ ∃ x φ ∨ ∃ y ψ
13 5 12 bitri ⊢ ∃ x ∃ y φ ∨ ∃ y ψ ↔ ∃ x φ ∨ ∃ y ψ
14 4 13 bitri ⊢ ∃ x ∃ y φ ∨ ψ ↔ ∃ x φ ∨ ∃ y ψ