This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iunin2

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

Ref Expression
Assertion iunin2 ⊢ ⋃ x ∈ A B ∩ C = B ∩ ⋃ x ∈ A C

Proof

Step Hyp Ref Expression
1 r19.42v ⊢ ∃ x ∈ A y ∈ B ∧ y ∈ C ↔ y ∈ B ∧ ∃ x ∈ A y ∈ C
2 elin ⊢ y ∈ B ∩ C ↔ y ∈ B ∧ y ∈ C
3 2 rexbii ⊢ ∃ x ∈ A y ∈ B ∩ C ↔ ∃ x ∈ A y ∈ B ∧ y ∈ C
4 eliun ⊢ y ∈ ⋃ x ∈ A C ↔ ∃ x ∈ A y ∈ C
5 4 anbi2i ⊢ y ∈ B ∧ y ∈ ⋃ x ∈ A C ↔ y ∈ B ∧ ∃ x ∈ A y ∈ C
6 1 3 5 3bitr4i ⊢ ∃ x ∈ A y ∈ B ∩ C ↔ y ∈ B ∧ y ∈ ⋃ x ∈ A C
7 eliun ⊢ y ∈ ⋃ x ∈ A B ∩ C ↔ ∃ x ∈ A y ∈ B ∩ C
8 elin ⊢ y ∈ B ∩ ⋃ x ∈ A C ↔ y ∈ B ∧ y ∈ ⋃ x ∈ A C
9 6 7 8 3bitr4i ⊢ y ∈ ⋃ x ∈ A B ∩ C ↔ y ∈ B ∩ ⋃ x ∈ A C
10 9 eqriv ⊢ ⋃ x ∈ A B ∩ C = B ∩ ⋃ x ∈ A C