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 ∈ A B = ⋃ x ∈ A ran ⁡ B

Proof

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