Metamath Proof Explorer

Theorem iunun

Description: Separate a union in an indexed union. (Contributed by NM, 27-Dec-2004) (Proof shortened by Mario Carneiro, 17-Nov-2016)

Ref Expression
Assertion iunun ⊢⋃x∈AB∪C=⋃x∈AB∪⋃x∈AC

Proof

Step Hyp Ref Expression
1 r19.43 ⊢∃x∈Ay∈B∨y∈C↔∃x∈Ay∈B∨∃x∈Ay∈C
2 elun ⊢y∈B∪C↔y∈B∨y∈C
3 2 rexbii ⊢∃x∈Ay∈B∪C↔∃x∈Ay∈B∨y∈C
4 eliun ⊢y∈⋃x∈AB↔∃x∈Ay∈B
5 eliun ⊢y∈⋃x∈AC↔∃x∈Ay∈C
6 4 5 orbi12i ⊢y∈⋃x∈AB∨y∈⋃x∈AC↔∃x∈Ay∈B∨∃x∈Ay∈C
7 1 3 6 3bitr4i ⊢∃x∈Ay∈B∪C↔y∈⋃x∈AB∨y∈⋃x∈AC
8 eliun ⊢y∈⋃x∈AB∪C↔∃x∈Ay∈B∪C
9 elun ⊢y∈⋃x∈AB∪⋃x∈AC↔y∈⋃x∈AB∨y∈⋃x∈AC
10 7 8 9 3bitr4i ⊢y∈⋃x∈AB∪C↔y∈⋃x∈AB∪⋃x∈AC
11 10 eqriv ⊢⋃x∈AB∪C=⋃x∈AB∪⋃x∈AC