Theorem iunxiun 4049

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

Assertion

Ref	Expression
iunxiun	|- U_x e. U_ y e. A BC = U_y e. A U_x e. B C

Distinct variable groups:   x,y   x,A   y,C

Allowed substitution hints:   A(y)   B(x,y)   C(x)

Proof of Theorem iunxiun

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eliun 3974	. . . . . . . 8 |- (x e. U_y e. A B <-> E.y e. A x e. B)
2	1	anbi1i 676	. . . . . . 7 |- ((x e. U_y e. A B /\ z e. C) <-> (E.y e. A x e. B /\ z e. C))
3		r19.41v 2765	. . . . . . 7 |- (E.y e. A (x e. B /\ z e. C) <-> (E.y e. A x e. B /\ z e. C))
4	2, 3	bitr4i 243	. . . . . 6 |- ((x e. U_y e. A B /\ z e. C) <-> E.y e. A (x e. B /\ z e. C))
5	4	exbii 1582	. . . . 5 |- (E.x(x e. U_y e. A B /\ z e. C) <-> E.xE.y e. A (x e. B /\ z e. C))
6		rexcom4 2879	. . . . 5 |- (E.y e. A E.x(x e. B /\ z e. C) <-> E.xE.y e. A (x e. B /\ z e. C))
7	5, 6	bitr4i 243	. . . 4 |- (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 2621	. . . 4 |- (E.x e. U_ y e. A Bz e. C <-> E.x(x e. U_y e. A B /\ z e. C))
9		eliun 3974	. . . . . 6 |- (z e. U_x e. B C <-> E.x e. B z e. C)
10		df-rex 2621	. . . . . 6 |- (E.x e. B z e. C <-> E.x(x e. B /\ z e. C))
11	9, 10	bitri 240	. . . . 5 |- (z e. U_x e. B C <-> E.x(x e. B /\ z e. C))
12	11	rexbii 2640	. . . 4 |- (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 268	. . 3 |- (E.x e. U_ y e. A Bz e. C <-> E.y e. A z e. U_x e. B C)
14		eliun 3974	. . 3 |- (z e. U_x e. U_ y e. A BC <-> E.x e. U_ y e. A Bz e. C)
15		eliun 3974	. . 3 |- (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 268	. 2 |- (z e. U_x e. U_ y e. A BC <-> z e. U_y e. A U_x e. B C)
17	16	eqriv 2350	1 |- U_x e. U_ y e. A BC = U_y e. A U_x e. B C

Syntax hints:   /\ wa 358  E.wex 1541   = wceq 1642   e. wcel 1710  E.wrex 2616  U_ciun 3970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ral 2620  df-rex 2621  df-v 2862  df-iun 3972

This theorem is referenced by: (None)