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 ⊢ Ⅎ 𝑦 𝜑
eeor.2 ⊢ Ⅎ 𝑥 𝜓
Assertion eeor ( ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∨ 𝜓 ) ↔ ( ∃ 𝑥 𝜑 ∨ ∃ 𝑦 𝜓 ) )

Proof

Step Hyp Ref Expression
1 eeor.1 ⊢ Ⅎ 𝑦 𝜑
2 eeor.2 ⊢ Ⅎ 𝑥 𝜓
3 19.43 ⊢ ( ∃ 𝑦 ( 𝜑 ∨ 𝜓 ) ↔ ( ∃ 𝑦 𝜑 ∨ ∃ 𝑦 𝜓 ) )
4 3 exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∨ 𝜓 ) ↔ ∃ 𝑥 ( ∃ 𝑦 𝜑 ∨ ∃ 𝑦 𝜓 ) )
5 19.43 ⊢ ( ∃ 𝑥 ( ∃ 𝑦 𝜑 ∨ ∃ 𝑦 𝜓 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∨ ∃ 𝑥 ∃ 𝑦 𝜓 ) )
6 1 19.9 ⊢ ( ∃ 𝑦 𝜑 ↔ 𝜑 )
7 6 exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑥 𝜑 )
8 excom ⊢ ( ∃ 𝑥 ∃ 𝑦 𝜓 ↔ ∃ 𝑦 ∃ 𝑥 𝜓 )
9 2 19.9 ⊢ ( ∃ 𝑥 𝜓 ↔ 𝜓 )
10 9 exbii ⊢ ( ∃ 𝑦 ∃ 𝑥 𝜓 ↔ ∃ 𝑦 𝜓 )
11 8 10 bitri ⊢ ( ∃ 𝑥 ∃ 𝑦 𝜓 ↔ ∃ 𝑦 𝜓 )
12 7 11 orbi12i ⊢ ( ( ∃ 𝑥 ∃ 𝑦 𝜑 ∨ ∃ 𝑥 ∃ 𝑦 𝜓 ) ↔ ( ∃ 𝑥 𝜑 ∨ ∃ 𝑦 𝜓 ) )
13 5 12 bitri ⊢ ( ∃ 𝑥 ( ∃ 𝑦 𝜑 ∨ ∃ 𝑦 𝜓 ) ↔ ( ∃ 𝑥 𝜑 ∨ ∃ 𝑦 𝜓 ) )
14 4 13 bitri ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∨ 𝜓 ) ↔ ( ∃ 𝑥 𝜑 ∨ ∃ 𝑦 𝜓 ) )