Theorem iuncom

Description: Commutation of indexed unions. (Contributed by NM, 18-Dec-2008)

	Ref	Expression
Assertion	iuncom	$$⊢\bigcup _{x\in A}\bigcup _{y\in B}C=\bigcup _{y\in B}\bigcup _{x\in A}C$$

Proof

Step	Hyp	Ref	Expression
1		rexcom	$$⊢\exists x\in A\exists y\in Bz\in C\leftrightarrow \exists y\in B\exists x\in Az\in C$$
2		eliun	$$⊢z\in \bigcup _{y\in B}C\leftrightarrow \exists y\in Bz\in C$$
3	2	rexbii	$$⊢\exists x\in Az\in \bigcup _{y\in B}C\leftrightarrow \exists x\in A\exists y\in Bz\in C$$
4		eliun	$$⊢z\in \bigcup _{x\in A}C\leftrightarrow \exists x\in Az\in C$$
5	4	rexbii	$$⊢\exists y\in Bz\in \bigcup _{x\in A}C\leftrightarrow \exists y\in B\exists x\in Az\in C$$
6	1 3 5	3bitr4i	$$⊢\exists x\in Az\in \bigcup _{y\in B}C\leftrightarrow \exists y\in Bz\in \bigcup _{x\in A}C$$
7		eliun	$$⊢z\in \bigcup _{x\in A}\bigcup _{y\in B}C\leftrightarrow \exists x\in Az\in \bigcup _{y\in B}C$$
8		eliun	$$⊢z\in \bigcup _{y\in B}\bigcup _{x\in A}C\leftrightarrow \exists y\in Bz\in \bigcup _{x\in A}C$$
9	6 7 8	3bitr4i	$$⊢z\in \bigcup _{x\in A}\bigcup _{y\in B}C\leftrightarrow z\in \bigcup _{y\in B}\bigcup _{x\in A}C$$
10	9	eqriv	$$⊢\bigcup _{x\in A}\bigcup _{y\in B}C=\bigcup _{y\in B}\bigcup _{x\in A}C$$