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 e. _V
	iunex.2	|- B e. _V
Assertion	iunex	|- U_ x e. A B e. _V

Proof

Step	Hyp	Ref	Expression
1		iunex.1	|- A e. _V
2		iunex.2	|- B e. _V
3	2	rgenw	|- A. x e. A B e. _V
4		iunexg	|- ( ( A e. _V /\ A. x e. A B e. _V ) -> U_ x e. A B e. _V )
5	1 3 4	mp2an	|- U_ x e. A B e. _V