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 φ ↔ ∃ x x ∈ A ∪ B ∧ φ
2 19.43 ⊢ ∃ x x ∈ A ∧ φ ∨ x ∈ B ∧ φ ↔ ∃ x x ∈ A ∧ φ ∨ ∃ x x ∈ 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 ⊢ ∃ x x ∈ A ∪ B ∧ φ ↔ ∃ x x ∈ A ∧ φ ∨ x ∈ B ∧ φ
8 df-rex ⊢ ∃ x ∈ A φ ↔ ∃ x x ∈ A ∧ φ
9 df-rex ⊢ ∃ x ∈ B φ ↔ ∃ x x ∈ B ∧ φ
10 8 9 orbi12i ⊢ ∃ x ∈ A φ ∨ ∃ x ∈ B φ ↔ ∃ x x ∈ A ∧ φ ∨ ∃ x x ∈ B ∧ φ
11 2 7 10 3bitr4i ⊢ ∃ x x ∈ A ∪ B ∧ φ ↔ ∃ x ∈ A φ ∨ ∃ x ∈ B φ
12 1 11 bitri ⊢ ∃ x ∈ A ∪ B φ ↔ ∃ x ∈ A φ ∨ ∃ x ∈ B φ