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∈AB

Proof

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