Theorem iunexg

Description: The existence of an indexed union. x is normally a free-variable parameter in B . (Contributed by NM, 23-Mar-2006)

	Ref	Expression
Assertion	iunexg	$$⊢\left(A\in V\wedge \forall x\in AB\in W\right)\to \bigcup _{x\in A}B\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		dfiun2g	$$⊢\forall x\in AB\in W\to \bigcup _{x\in A}B=\bigcup \left\{y|\exists x\in Ay=B\right\}$$
2	1	adantl	$$⊢\left(A\in V\wedge \forall x\in AB\in W\right)\to \bigcup _{x\in A}B=\bigcup \left\{y|\exists x\in Ay=B\right\}$$
3		abrexexg	$$⊢A\in V\to \left\{y|\exists x\in Ay=B\right\}\in \mathrm{V}$$
4	3	uniexd	$$⊢A\in V\to \bigcup \left\{y|\exists x\in Ay=B\right\}\in \mathrm{V}$$
5	4	adantr	$$⊢\left(A\in V\wedge \forall x\in AB\in W\right)\to \bigcup \left\{y|\exists x\in Ay=B\right\}\in \mathrm{V}$$
6	2 5	eqeltrd	$$⊢\left(A\in V\wedge \forall x\in AB\in W\right)\to \bigcup _{x\in A}B\in \mathrm{V}$$