# Metamath Proof Explorer

## Theorem dfiunv2

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

Ref Expression
Assertion dfiunv2 ${⊢}\bigcup _{{x}\in {A}}\bigcup _{{y}\in {B}}{C}=\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}\in {C}\right\}$

### Proof

Step Hyp Ref Expression
1 df-iun ${⊢}\bigcup _{{y}\in {B}}{C}=\left\{{w}|\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{w}\in {C}\right\}$
2 1 a1i ${⊢}{x}\in {A}\to \bigcup _{{y}\in {B}}{C}=\left\{{w}|\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{w}\in {C}\right\}$
3 2 iuneq2i ${⊢}\bigcup _{{x}\in {A}}\bigcup _{{y}\in {B}}{C}=\bigcup _{{x}\in {A}}\left\{{w}|\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{w}\in {C}\right\}$
4 df-iun ${⊢}\bigcup _{{x}\in {A}}\left\{{w}|\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{w}\in {C}\right\}=\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in \left\{{w}|\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{w}\in {C}\right\}\right\}$
5 vex ${⊢}{z}\in \mathrm{V}$
6 eleq1w ${⊢}{w}={z}\to \left({w}\in {C}↔{z}\in {C}\right)$
7 6 rexbidv ${⊢}{w}={z}\to \left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{w}\in {C}↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}\in {C}\right)$
8 5 7 elab ${⊢}{z}\in \left\{{w}|\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{w}\in {C}\right\}↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}\in {C}$
9 8 rexbii ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in \left\{{w}|\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{w}\in {C}\right\}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}\in {C}$
10 9 abbii ${⊢}\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in \left\{{w}|\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{w}\in {C}\right\}\right\}=\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}\in {C}\right\}$
11 3 4 10 3eqtri ${⊢}\bigcup _{{x}\in {A}}\bigcup _{{y}\in {B}}{C}=\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}\in {C}\right\}$