Theorem iunxpf

Description: Indexed union on a Cartesian product equals a double indexed union. The hypothesis specifies an implicit substitution. (Contributed by NM, 19-Dec-2008)

	Ref	Expression
Hypotheses	iunxpf.1	$$⊢\underset{\_}{Ⅎ}yC$$
	iunxpf.2	$$⊢\underset{\_}{Ⅎ}zC$$
	iunxpf.3	$$⊢\underset{\_}{Ⅎ}xD$$
	iunxpf.4	$$⊢x=⟨y,z⟩\to C=D$$
Assertion	iunxpf	$$⊢\bigcup _{x\in A\times B}C=\bigcup _{y\in A}\bigcup _{z\in B}D$$

Proof

Step	Hyp	Ref	Expression
1		iunxpf.1	$$⊢\underset{\_}{Ⅎ}yC$$
2		iunxpf.2	$$⊢\underset{\_}{Ⅎ}zC$$
3		iunxpf.3	$$⊢\underset{\_}{Ⅎ}xD$$
4		iunxpf.4	$$⊢x=⟨y,z⟩\to C=D$$
5	1	nfcri	$$⊢Ⅎyw\in C$$
6	2	nfcri	$$⊢Ⅎzw\in C$$
7	3	nfcri	$$⊢Ⅎxw\in D$$
8	4	eleq2d	$$⊢x=⟨y,z⟩\to \left(w\in C\leftrightarrow w\in D\right)$$
9	5 6 7 8	rexxpf	$$⊢\exists x\in \left(A\times B\right)w\in C\leftrightarrow \exists y\in A\exists z\in Bw\in D$$
10		eliun	$$⊢w\in \bigcup _{x\in A\times B}C\leftrightarrow \exists x\in \left(A\times B\right)w\in C$$
11		eliun	$$⊢w\in \bigcup _{y\in A}\bigcup _{z\in B}D\leftrightarrow \exists y\in Aw\in \bigcup _{z\in B}D$$
12		eliun	$$⊢w\in \bigcup _{z\in B}D\leftrightarrow \exists z\in Bw\in D$$
13	12	rexbii	$$⊢\exists y\in Aw\in \bigcup _{z\in B}D\leftrightarrow \exists y\in A\exists z\in Bw\in D$$
14	11 13	bitri	$$⊢w\in \bigcup _{y\in A}\bigcup _{z\in B}D\leftrightarrow \exists y\in A\exists z\in Bw\in D$$
15	9 10 14	3bitr4i	$$⊢w\in \bigcup _{x\in A\times B}C\leftrightarrow w\in \bigcup _{y\in A}\bigcup _{z\in B}D$$
16	15	eqriv	$$⊢\bigcup _{x\in A\times B}C=\bigcup _{y\in A}\bigcup _{z\in B}D$$