Metamath Proof Explorer


Theorem dfiunv2

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

Ref Expression
Assertion dfiunv2 xAyBC=z|xAyBzC

Proof

Step Hyp Ref Expression
1 df-iun yBC=w|yBwC
2 1 a1i xAyBC=w|yBwC
3 2 iuneq2i xAyBC=xAw|yBwC
4 df-iun xAw|yBwC=z|xAzw|yBwC
5 vex zV
6 eleq1w w=zwCzC
7 6 rexbidv w=zyBwCyBzC
8 5 7 elab zw|yBwCyBzC
9 8 rexbii xAzw|yBwCxAyBzC
10 9 abbii z|xAzw|yBwC=z|xAyBzC
11 3 4 10 3eqtri xAyBC=z|xAyBzC