Theorem iunxiun

Description: Separate an indexed union in the index of an indexed union. (Contributed by Mario Carneiro, 5-Dec-2016)

	Ref	Expression
Assertion	iunxiun	|- U_ x e. U_ y e. A B C = U_ y e. A U_ x e. B C

Proof

Step	Hyp	Ref	Expression
1		eliun	|- ( x e. U_ y e. A B <-> E. y e. A x e. B )
2	1	anbi1i	|- ( ( x e. U_ y e. A B /\ z e. C ) <-> ( E. y e. A x e. B /\ z e. C ) )
3		r19.41v	|- ( E. y e. A ( x e. B /\ z e. C ) <-> ( E. y e. A x e. B /\ z e. C ) )
4	2 3	bitr4i	|- ( ( x e. U_ y e. A B /\ z e. C ) <-> E. y e. A ( x e. B /\ z e. C ) )
5	4	exbii	|- ( E. x ( x e. U_ y e. A B /\ z e. C ) <-> E. x E. y e. A ( x e. B /\ z e. C ) )
6		rexcom4	|- ( E. y e. A E. x ( x e. B /\ z e. C ) <-> E. x E. y e. A ( x e. B /\ z e. C ) )
7	5 6	bitr4i	|- ( E. x ( x e. U_ y e. A B /\ z e. C ) <-> E. y e. A E. x ( x e. B /\ z e. C ) )
8		df-rex	|- ( E. x e. U_ y e. A B z e. C <-> E. x ( x e. U_ y e. A B /\ z e. C ) )
9		eliun	|- ( z e. U_ x e. B C <-> E. x e. B z e. C )
10		df-rex	|- ( E. x e. B z e. C <-> E. x ( x e. B /\ z e. C ) )
11	9 10	bitri	|- ( z e. U_ x e. B C <-> E. x ( x e. B /\ z e. C ) )
12	11	rexbii	|- ( E. y e. A z e. U_ x e. B C <-> E. y e. A E. x ( x e. B /\ z e. C ) )
13	7 8 12	3bitr4i	|- ( E. x e. U_ y e. A B z e. C <-> E. y e. A z e. U_ x e. B C )
14		eliun	|- ( z e. U_ x e. U_ y e. A B C <-> E. x e. U_ y e. A B z e. C )
15		eliun	|- ( z e. U_ y e. A U_ x e. B C <-> E. y e. A z e. U_ x e. B C )
16	13 14 15	3bitr4i	|- ( z e. U_ x e. U_ y e. A B C <-> z e. U_ y e. A U_ x e. B C )
17	16	eqriv	|- U_ x e. U_ y e. A B C = U_ y e. A U_ x e. B C