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	|- ( ( A e. V /\ A. x e. A B e. W ) -> U_ x e. A B e. _V )

Proof

Step	Hyp	Ref	Expression
1		dfiun2g	|- ( A. x e. A B e. W -> U_ x e. A B = U. { y | E. x e. A y = B } )
2	1	adantl	|- ( ( A e. V /\ A. x e. A B e. W ) -> U_ x e. A B = U. { y | E. x e. A y = B } )
3		abrexexg	|- ( A e. V -> { y | E. x e. A y = B } e. _V )
4	3	uniexd	|- ( A e. V -> U. { y | E. x e. A y = B } e. _V )
5	4	adantr	|- ( ( A e. V /\ A. x e. A B e. W ) -> U. { y | E. x e. A y = B } e. _V )
6	2 5	eqeltrd	|- ( ( A e. V /\ A. x e. A B e. W ) -> U_ x e. A B e. _V )