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	|- F/_ y C
	iunxpf.2	|- F/_ z C
	iunxpf.3	|- F/_ x D
	iunxpf.4	|- ( x = <. y , z >. -> C = D )
Assertion	iunxpf	|- U_ x e. ( A X. B ) C = U_ y e. A U_ z e. B D

Proof

Step	Hyp	Ref	Expression
1		iunxpf.1	|- F/_ y C
2		iunxpf.2	|- F/_ z C
3		iunxpf.3	|- F/_ x D
4		iunxpf.4	|- ( x = <. y , z >. -> C = D )
5	1	nfcri	|- F/ y w e. C
6	2	nfcri	|- F/ z w e. C
7	3	nfcri	|- F/ x w e. D
8	4	eleq2d	|- ( x = <. y , z >. -> ( w e. C <-> w e. D ) )
9	5 6 7 8	rexxpf	|- ( E. x e. ( A X. B ) w e. C <-> E. y e. A E. z e. B w e. D )
10		eliun	|- ( w e. U_ x e. ( A X. B ) C <-> E. x e. ( A X. B ) w e. C )
11		eliun	|- ( w e. U_ y e. A U_ z e. B D <-> E. y e. A w e. U_ z e. B D )
12		eliun	|- ( w e. U_ z e. B D <-> E. z e. B w e. D )
13	12	rexbii	|- ( E. y e. A w e. U_ z e. B D <-> E. y e. A E. z e. B w e. D )
14	11 13	bitri	|- ( w e. U_ y e. A U_ z e. B D <-> E. y e. A E. z e. B w e. D )
15	9 10 14	3bitr4i	|- ( w e. U_ x e. ( A X. B ) C <-> w e. U_ y e. A U_ z e. B D )
16	15	eqriv	|- U_ x e. ( A X. B ) C = U_ y e. A U_ z e. B D