Theorem dfiun2

Description: Alternate definition of indexed union when B is a set. Definition 15(a) of Suppes p. 44. (Contributed by NM, 27-Jun-1998) (Revised by David Abernethy, 19-Jun-2012)

	Ref	Expression
Hypothesis	dfiun2.1	$$⊢B\in \mathrm{V}$$
Assertion	dfiun2	$$⊢\bigcup _{x\in A}B=\bigcup \left\{y|\exists x\in Ay=B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfiun2.1	$$⊢B\in \mathrm{V}$$
2		dfiun2g	$$⊢\forall x\in AB\in \mathrm{V}\to \bigcup _{x\in A}B=\bigcup \left\{y|\exists x\in Ay=B\right\}$$
3	1	a1i	$$⊢x\in A\to B\in \mathrm{V}$$
4	2 3	mprg	$$⊢\bigcup _{x\in A}B=\bigcup \left\{y|\exists x\in Ay=B\right\}$$