This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfiun3g

Description: Alternate definition of indexed union when B is a set. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion dfiun3g ⊢ ∀ x ∈ A B ∈ C → ⋃ x ∈ A B = ⋃ ran ⁡ x ∈ A ⟼ B

Proof

Step Hyp Ref Expression
1 dfiun2g ⊢ ∀ x ∈ A B ∈ C → ⋃ x ∈ A B = ⋃ y | ∃ x ∈ A y = B
2 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
3 2 rnmpt ⊢ ran ⁡ x ∈ A ⟼ B = y | ∃ x ∈ A y = B
4 3 unieqi ⊢ ⋃ ran ⁡ x ∈ A ⟼ B = ⋃ y | ∃ x ∈ A y = B
5 1 4 eqtr4di ⊢ ∀ x ∈ A B ∈ C → ⋃ x ∈ A B = ⋃ ran ⁡ x ∈ A ⟼ B