Metamath Proof Explorer

Theorem rniun

Description: The range of an indexed union. (Contributed by Mario Carneiro, 29-May-2015)

Ref Expression
Assertion rniun ⊢ran⁡⋃x∈AB=⋃x∈Aran⁡B

Proof

Step Hyp Ref Expression
1 rexcom4 ⊢∃x∈A∃yyz∈B↔∃y∃x∈Ayz∈B
2 vex ⊢z∈V
3 2 elrn2 ⊢z∈ran⁡B↔∃yyz∈B
4 3 rexbii ⊢∃x∈Az∈ran⁡B↔∃x∈A∃yyz∈B
5 eliun ⊢yz∈⋃x∈AB↔∃x∈Ayz∈B
6 5 exbii ⊢∃yyz∈⋃x∈AB↔∃y∃x∈Ayz∈B
7 1 4 6 3bitr4ri ⊢∃yyz∈⋃x∈AB↔∃x∈Az∈ran⁡B
8 2 elrn2 ⊢z∈ran⁡⋃x∈AB↔∃yyz∈⋃x∈AB
9 eliun ⊢z∈⋃x∈Aran⁡B↔∃x∈Az∈ran⁡B
10 7 8 9 3bitr4i ⊢z∈ran⁡⋃x∈AB↔z∈⋃x∈Aran⁡B
11 10 eqriv ⊢ran⁡⋃x∈AB=⋃x∈Aran⁡B