Theorem dfiun3

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

	Ref	Expression
Hypothesis	dfiun3.1	⊢ 𝐵 ∈ V
Assertion	dfiun3	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		dfiun3.1	⊢ 𝐵 ∈ V
2		dfiun3g	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
3	1	a1i	⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ∈ V )
4	2 3	mprg	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )