Metamath Proof Explorer

Theorem rexun

Description: Restricted existential quantification over union. (Contributed by Jeff Madsen, 5-Jan-2011)

Ref Expression
Assertion rexun ⊢∃x∈A∪Bφ↔∃x∈Aφ∨∃x∈Bφ

Proof

Step Hyp Ref Expression
1 df-rex ⊢∃x∈A∪Bφ↔∃xx∈A∪B∧φ
2 19.43 ⊢∃xx∈A∧φ∨x∈B∧φ↔∃xx∈A∧φ∨∃xx∈B∧φ
3 elun ⊢x∈A∪B↔x∈A∨x∈B
4 3 anbi1i ⊢x∈A∪B∧φ↔x∈A∨x∈B∧φ
5 andir ⊢x∈A∨x∈B∧φ↔x∈A∧φ∨x∈B∧φ
6 4 5 bitri ⊢x∈A∪B∧φ↔x∈A∧φ∨x∈B∧φ
7 6 exbii ⊢∃xx∈A∪B∧φ↔∃xx∈A∧φ∨x∈B∧φ
8 df-rex ⊢∃x∈Aφ↔∃xx∈A∧φ
9 df-rex ⊢∃x∈Bφ↔∃xx∈B∧φ
10 8 9 orbi12i ⊢∃x∈Aφ∨∃x∈Bφ↔∃xx∈A∧φ∨∃xx∈B∧φ
11 2 7 10 3bitr4i ⊢∃xx∈A∪B∧φ↔∃x∈Aφ∨∃x∈Bφ
12 1 11 bitri ⊢∃x∈A∪Bφ↔∃x∈Aφ∨∃x∈Bφ