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\exists y\in Bz\in C\right\}$$

Proof

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