Metamath Proof Explorer

Theorem iunxiun

Description: Separate an indexed union in the index of an indexed union. (Contributed by Mario Carneiro, 5-Dec-2016)

Ref Expression
Assertion iunxiun ⊢ ⋃ x ∈ ⋃ y ∈ A B C = ⋃ y ∈ A ⋃ x ∈ B C

Proof

Step Hyp Ref Expression
1 eliun ⊢ x ∈ ⋃ y ∈ A B ↔ ∃ y ∈ A x ∈ B
2 1 anbi1i ⊢ x ∈ ⋃ y ∈ A B ∧ z ∈ C ↔ ∃ y ∈ A x ∈ B ∧ z ∈ C
3 r19.41v ⊢ ∃ y ∈ A x ∈ B ∧ z ∈ C ↔ ∃ y ∈ A x ∈ B ∧ z ∈ C
4 2 3 bitr4i ⊢ x ∈ ⋃ y ∈ A B ∧ z ∈ C ↔ ∃ y ∈ A x ∈ B ∧ z ∈ C
5 4 exbii ⊢ ∃ x x ∈ ⋃ y ∈ A B ∧ z ∈ C ↔ ∃ x ∃ y ∈ A x ∈ B ∧ z ∈ C
6 rexcom4 ⊢ ∃ y ∈ A ∃ x x ∈ B ∧ z ∈ C ↔ ∃ x ∃ y ∈ A x ∈ B ∧ z ∈ C
7 5 6 bitr4i ⊢ ∃ x x ∈ ⋃ y ∈ A B ∧ z ∈ C ↔ ∃ y ∈ A ∃ x x ∈ B ∧ z ∈ C
8 df-rex ⊢ ∃ x ∈ ⋃ y ∈ A B z ∈ C ↔ ∃ x x ∈ ⋃ y ∈ A B ∧ z ∈ C
9 eliun ⊢ z ∈ ⋃ x ∈ B C ↔ ∃ x ∈ B z ∈ C
10 df-rex ⊢ ∃ x ∈ B z ∈ C ↔ ∃ x x ∈ B ∧ z ∈ C
11 9 10 bitri ⊢ z ∈ ⋃ x ∈ B C ↔ ∃ x x ∈ B ∧ z ∈ C
12 11 rexbii ⊢ ∃ y ∈ A z ∈ ⋃ x ∈ B C ↔ ∃ y ∈ A ∃ x x ∈ B ∧ z ∈ C
13 7 8 12 3bitr4i ⊢ ∃ x ∈ ⋃ y ∈ A B z ∈ C ↔ ∃ y ∈ A z ∈ ⋃ x ∈ B C
14 eliun ⊢ z ∈ ⋃ x ∈ ⋃ y ∈ A B C ↔ ∃ x ∈ ⋃ y ∈ A B z ∈ C
15 eliun ⊢ z ∈ ⋃ y ∈ A ⋃ x ∈ B C ↔ ∃ y ∈ A z ∈ ⋃ x ∈ B C
16 13 14 15 3bitr4i ⊢ z ∈ ⋃ x ∈ ⋃ y ∈ A B C ↔ z ∈ ⋃ y ∈ A ⋃ x ∈ B C
17 16 eqriv ⊢ ⋃ x ∈ ⋃ y ∈ A B C = ⋃ y ∈ A ⋃ x ∈ B C