Theorem dfiun3g

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

	Ref	Expression
Assertion	dfiun3g	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		dfiun2g	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )
2		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
3	2	rnmpt	⊢ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 }
4	3	unieqi	⊢ ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 }
5	1 4	eqtr4di	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )