Metamath Proof Explorer

Theorem iuncom

Description: Commutation of indexed unions. (Contributed by NM, 18-Dec-2008)

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

Proof

Step Hyp Ref Expression
1 rexcom ⊢ ∃ x ∈ A ∃ y ∈ B z ∈ C ↔ ∃ y ∈ B ∃ x ∈ A z ∈ C
2 eliun ⊢ z ∈ ⋃ y ∈ B C ↔ ∃ y ∈ B z ∈ C
3 2 rexbii ⊢ ∃ x ∈ A z ∈ ⋃ y ∈ B C ↔ ∃ x ∈ A ∃ y ∈ B z ∈ C
4 eliun ⊢ z ∈ ⋃ x ∈ A C ↔ ∃ x ∈ A z ∈ C
5 4 rexbii ⊢ ∃ y ∈ B z ∈ ⋃ x ∈ A C ↔ ∃ y ∈ B ∃ x ∈ A z ∈ C
6 1 3 5 3bitr4i ⊢ ∃ x ∈ A z ∈ ⋃ y ∈ B C ↔ ∃ y ∈ B z ∈ ⋃ x ∈ A C
7 eliun ⊢ z ∈ ⋃ x ∈ A ⋃ y ∈ B C ↔ ∃ x ∈ A z ∈ ⋃ y ∈ B C
8 eliun ⊢ z ∈ ⋃ y ∈ B ⋃ x ∈ A C ↔ ∃ y ∈ B z ∈ ⋃ x ∈ A C
9 6 7 8 3bitr4i ⊢ z ∈ ⋃ x ∈ A ⋃ y ∈ B C ↔ z ∈ ⋃ y ∈ B ⋃ x ∈ A C
10 9 eqriv ⊢ ⋃ x ∈ A ⋃ y ∈ B C = ⋃ y ∈ B ⋃ x ∈ A C