Theorem iunxun 4350

Description: Separate a union in the index of an indexed union. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)

Assertion

Ref	Expression
iunxun	|- U_ x e. ( A u. B ) C = ( U_ x e. A C u. U_ x e. B C )

Proof of Theorem iunxun

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rexun 3634	. . . 4 |- ( E. x e. ( A u. B ) y e. C <-> ( E. x e. A y e. C \/ E. x e. B y e. C ) )
2		eliun 4273	. . . . 5 |- ( y e. U_ x e. A C <-> E. x e. A y e. C )
3		eliun 4273	. . . . 5 |- ( y e. U_ x e. B C <-> E. x e. B y e. C )
4	2, 3	orbi12i 521	. . . 4 |- ( ( y e. U_ x e. A C \/ y e. U_ x e. B C ) <-> ( E. x e. A y e. C \/ E. x e. B y e. C ) )
5	1, 4	bitr4i 252	. . 3 |- ( E. x e. ( A u. B ) y e. C <-> ( y e. U_ x e. A C \/ y e. U_ x e. B C ) )
6		eliun 4273	. . 3 |- ( y e. U_ x e. ( A u. B ) C <-> E. x e. ( A u. B ) y e. C )
7		elun 3595	. . 3 |- ( y e. ( U_ x e. A C u. U_ x e. B C ) <-> ( y e. U_ x e. A C \/ y e. U_ x e. B C ) )
8	5, 6, 7	3bitr4i 277	. 2 |- ( y e. U_ x e. ( A u. B ) C <-> y e. ( U_ x e. A C u. U_ x e. B C ) )
9	8	eqriv 2447	1 |- U_ x e. ( A u. B ) C = ( U_ x e. A C u. U_ x e. B C )

Syntax hints:   \/ wo 368   = wceq 1370   e. wcel 1758   E.wrex 2796   u. cun 3424   U_ciun 4269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-rex 2801  df-v 3070  df-un 3431  df-iun 4271

This theorem is referenced by:  iunsuc  4899  funiunfv  6064  iunfi  7700  kmlem11  8430  ackbij1lem9  8498  fsum2dlem  13339  fsumiun  13386  prmreclem4  14082  fiuncmp  19123  ovolfiniun  21100  finiunmbl  21141  volfiniun  21144  voliunlem1  21147  uniioombllem4  21182  iuninc  26045  ofpreima2  26119  indval2  26605  sigaclfu2  26698  measvuni  26762  cvmliftlem10  27317  fprod2dlem  27625  mblfinlem2  28567  iunxprg  30272