Theorem iunex

Description: The existence of an indexed union. x is normally a free-variable parameter in the class expression substituted for B , which can be read informally as B ( x ) . (Contributed by NM, 13-Oct-2003)

	Ref	Expression
Hypotheses	iunex.1	$$⊢A\in \mathrm{V}$$
	iunex.2	$$⊢B\in \mathrm{V}$$
Assertion	iunex	$$⊢\bigcup _{x\in A}B\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		iunex.1	$$⊢A\in \mathrm{V}$$
2		iunex.2	$$⊢B\in \mathrm{V}$$
3	2	rgenw	$$⊢\forall x\in AB\in \mathrm{V}$$
4		iunexg	$$⊢\left(A\in \mathrm{V}\wedge \forall x\in AB\in \mathrm{V}\right)\to \bigcup _{x\in A}B\in \mathrm{V}$$
5	1 3 4	mp2an	$$⊢\bigcup _{x\in A}B\in \mathrm{V}$$