Metamath Proof Explorer

Theorem iuncom4

Description: Commutation of union with indexed union. (Contributed by Mario Carneiro, 18-Jan-2014)

Ref Expression
Assertion iuncom4 ⊢ ⋃ x ∈ A ⋃ B = ⋃ ⋃ x ∈ A B

Proof

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