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 ∈ A B ∪ C = B ∪ ⋂ x ∈ A C

Proof

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