Theorem dfiunv2

Description: Define double indexed union. (Contributed by FL, 6-Nov-2013)

	Ref	Expression
Assertion	dfiunv2	|- U_ x e. A U_ y e. B C = { z | E. x e. A E. y e. B z e. C }

Proof

Step	Hyp	Ref	Expression
1		df-iun	|- U_ y e. B C = { w | E. y e. B w e. C }
2	1	a1i	|- ( x e. A -> U_ y e. B C = { w | E. y e. B w e. C } )
3	2	iuneq2i	|- U_ x e. A U_ y e. B C = U_ x e. A { w | E. y e. B w e. C }
4		df-iun	|- U_ x e. A { w | E. y e. B w e. C } = { z | E. x e. A z e. { w | E. y e. B w e. C } }
5		vex	|- z e. _V
6		eleq1w	|- ( w = z -> ( w e. C <-> z e. C ) )
7	6	rexbidv	|- ( w = z -> ( E. y e. B w e. C <-> E. y e. B z e. C ) )
8	5 7	elab	|- ( z e. { w | E. y e. B w e. C } <-> E. y e. B z e. C )
9	8	rexbii	|- ( E. x e. A z e. { w | E. y e. B w e. C } <-> E. x e. A E. y e. B z e. C )
10	9	abbii	|- { z | E. x e. A z e. { w | E. y e. B w e. C } } = { z | E. x e. A E. y e. B z e. C }
11	3 4 10	3eqtri	|- U_ x e. A U_ y e. B C = { z | E. x e. A E. y e. B z e. C }