Metamath Proof Explorer

Theorem iunxun

Description: Separate a union in the index of an indexed union. (Contributed by NM, 26-Mar-2004) (Proof shortened by Mario Carneiro, 17-Nov-2016)

Ref Expression
Assertion iunxun ⊢ ⋃ x ∈ A ∪ B C = ⋃ x ∈ A C ∪ ⋃ x ∈ B C

Proof

Step Hyp Ref Expression
1 rexun ⊢ ∃ x ∈ A ∪ B y ∈ C ↔ ∃ x ∈ A y ∈ C ∨ ∃ x ∈ B y ∈ C
2 eliun ⊢ y ∈ ⋃ x ∈ A C ↔ ∃ x ∈ A y ∈ C
3 eliun ⊢ y ∈ ⋃ x ∈ B C ↔ ∃ x ∈ B y ∈ C
4 2 3 orbi12i ⊢ y ∈ ⋃ x ∈ A C ∨ y ∈ ⋃ x ∈ B C ↔ ∃ x ∈ A y ∈ C ∨ ∃ x ∈ B y ∈ C
5 1 4 bitr4i ⊢ ∃ x ∈ A ∪ B y ∈ C ↔ y ∈ ⋃ x ∈ A C ∨ y ∈ ⋃ x ∈ B C
6 eliun ⊢ y ∈ ⋃ x ∈ A ∪ B C ↔ ∃ x ∈ A ∪ B y ∈ C
7 elun ⊢ y ∈ ⋃ x ∈ A C ∪ ⋃ x ∈ B C ↔ y ∈ ⋃ x ∈ A C ∨ y ∈ ⋃ x ∈ B C
8 5 6 7 3bitr4i ⊢ y ∈ ⋃ x ∈ A ∪ B C ↔ y ∈ ⋃ x ∈ A C ∪ ⋃ x ∈ B C
9 8 eqriv ⊢ ⋃ x ∈ A ∪ B C = ⋃ x ∈ A C ∪ ⋃ x ∈ B C