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

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

Proof

Step Hyp Ref Expression
1 r19.43 ⊢ ∃ x ∈ A y ∈ B ∨ y ∈ C ↔ ∃ x ∈ A y ∈ B ∨ ∃ x ∈ A y ∈ C
2 elun ⊢ 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 B ↔ ∃ x ∈ A y ∈ B
5 eliun ⊢ y ∈ ⋃ x ∈ A C ↔ ∃ x ∈ A y ∈ C
6 4 5 orbi12i ⊢ y ∈ ⋃ x ∈ A B ∨ y ∈ ⋃ x ∈ A C ↔ ∃ x ∈ A y ∈ B ∨ ∃ x ∈ A y ∈ C
7 1 3 6 3bitr4i ⊢ ∃ x ∈ A y ∈ B ∪ C ↔ y ∈ ⋃ x ∈ A B ∨ y ∈ ⋃ x ∈ A C
8 eliun ⊢ y ∈ ⋃ x ∈ A B ∪ C ↔ ∃ x ∈ A y ∈ B ∪ C
9 elun ⊢ y ∈ ⋃ x ∈ A B ∪ ⋃ x ∈ A C ↔ y ∈ ⋃ x ∈ A B ∨ y ∈ ⋃ x ∈ A C
10 7 8 9 3bitr4i ⊢ y ∈ ⋃ x ∈ A B ∪ C ↔ y ∈ ⋃ x ∈ A B ∪ ⋃ x ∈ A C
11 10 eqriv ⊢ ⋃ x ∈ A B ∪ C = ⋃ x ∈ A B ∪ ⋃ x ∈ A C