Theorem dfiun3g

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

	Ref	Expression
Assertion	dfiun3g	$$⊢\forall x\in AB\in C\to \bigcup _{x\in A}B=\bigcup \mathrm{ran}\left(x\in A⟼B\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfiun2g	$$⊢\forall x\in AB\in C\to \bigcup _{x\in A}B=\bigcup \left\{y|\exists x\in Ay=B\right\}$$
2		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
3	2	rnmpt	$$⊢\mathrm{ran}\left(x\in A⟼B\right)=\left\{y|\exists x\in Ay=B\right\}$$
4	3	unieqi	$$⊢\bigcup \mathrm{ran}\left(x\in A⟼B\right)=\bigcup \left\{y|\exists x\in Ay=B\right\}$$
5	1 4	eqtr4di	$$⊢\forall x\in AB\in C\to \bigcup _{x\in A}B=\bigcup \mathrm{ran}\left(x\in A⟼B\right)$$