Theorem iuniin

Description: Law combining indexed union with indexed intersection. Eq. 14 in KuratowskiMostowski p. 109. This theorem also appears as the last example at http://en.wikipedia.org/wiki/Union%5F%28set%5Ftheory%29 . (Contributed by NM, 17-Aug-2004) (Proof shortened by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	iuniin	|- U_ x e. A |^|_ y e. B C C_ |^|_ y e. B U_ x e. A C

Proof

Step	Hyp	Ref	Expression
1		r19.12	|- ( E. x e. A A. y e. B z e. C -> A. y e. B E. x e. A z e. C )
2		eliin	|- ( z e. _V -> ( z e. |^|_ y e. B C <-> A. y e. B z e. C ) )
3	2	elv	|- ( z e. |^|_ y e. B C <-> A. y e. B z e. C )
4	3	rexbii	|- ( E. x e. A z e. |^|_ y e. B C <-> E. x e. A A. y e. B z e. C )
5		eliun	|- ( z e. U_ x e. A C <-> E. x e. A z e. C )
6	5	ralbii	|- ( A. y e. B z e. U_ x e. A C <-> A. y e. B E. x e. A z e. C )
7	1 4 6	3imtr4i	|- ( E. x e. A z e. |^|_ y e. B C -> A. y e. B z e. U_ x e. A C )
8		eliun	|- ( z e. U_ x e. A |^|_ y e. B C <-> E. x e. A z e. |^|_ y e. B C )
9		eliin	|- ( z e. _V -> ( z e. |^|_ y e. B U_ x e. A C <-> A. y e. B z e. U_ x e. A C ) )
10	9	elv	|- ( z e. |^|_ y e. B U_ x e. A C <-> A. y e. B z e. U_ x e. A C )
11	7 8 10	3imtr4i	|- ( z e. U_ x e. A |^|_ y e. B C -> z e. |^|_ y e. B U_ x e. A C )
12	11	ssriv	|- U_ x e. A |^|_ y e. B C C_ |^|_ y e. B U_ x e. A C