Metamath Proof Explorer

Theorem iinun2

Description: Indexed intersection of union. Generalization of half of theorem "Distributive laws" in Enderton p. 30. Use intiin to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004)

Ref Expression
Assertion iinun2 ⊢⋂x∈AB∪C=B∪⋂x∈AC

Proof

Step Hyp Ref Expression
1 r19.32v ⊢∀x∈Ay∈B∨y∈C↔y∈B∨∀x∈Ay∈C
2 elun ⊢y∈B∪C↔y∈B∨y∈C
3 2 ralbii ⊢∀x∈Ay∈B∪C↔∀x∈Ay∈B∨y∈C
4 eliin ⊢y∈V→y∈⋂x∈AC↔∀x∈Ay∈C
5 4 elv ⊢y∈⋂x∈AC↔∀x∈Ay∈C
6 5 orbi2i ⊢y∈B∨y∈⋂x∈AC↔y∈B∨∀x∈Ay∈C
7 1 3 6 3bitr4i ⊢∀x∈Ay∈B∪C↔y∈B∨y∈⋂x∈AC
8 eliin ⊢y∈V→y∈⋂x∈AB∪C↔∀x∈Ay∈B∪C
9 8 elv ⊢y∈⋂x∈AB∪C↔∀x∈Ay∈B∪C
10 elun ⊢y∈B∪⋂x∈AC↔y∈B∨y∈⋂x∈AC
11 7 9 10 3bitr4i ⊢y∈⋂x∈AB∪C↔y∈B∪⋂x∈AC
12 11 eqriv ⊢⋂x∈AB∪C=B∪⋂x∈AC