This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 }