Theorem iunxun 4376

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 3625	. . . 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 4296	. . . . 5 |- ( y e. U_ x e. A C <-> E. x e. A y e. C )
3		eliun 4296	. . . . 5 |- ( y e. U_ x e. B C <-> E. x e. B y e. C )
4	2, 3	orbi12i 528	. . . 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 260	. . 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 4296	. . 3 |- ( y e. U_ x e. ( A u. B ) C <-> E. x e. ( A u. B ) y e. C )
7		elun 3585	. . 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 285	. 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 2458	1 |- U_ x e. ( A u. B ) C = ( U_ x e. A C u. U_ x e. B C )

Syntax hints:   \/ wo 374   = wceq 1454   e. wcel 1897   E.wrex 2749   u. cun 3413   U_ciun 4291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ral 2753  df-rex 2754  df-v 3058  df-un 3420  df-iun 4293

This theorem is referenced by:  iunsuc  5523  funiunfv  6177  iunfi  7887  kmlem11  8615  ackbij1lem9  8683  fsum2dlem  13879  fsumiun  13929  fprod2dlem  14082  prmreclem4  14911  fiuncmp  20467  ovolfiniun  22502  finiunmbl  22545  volfiniun  22548  voliunlem1  22551  uniioombllem4  22592  iunxdif3  28223  iuninc  28224  ofpreima2  28317  indval2  28884  esum2dlem  28961  sigaclfu2  28991  fiunelros  29044  measvuni  29084  cvmliftlem10  30065  mrsubvrs  30208  mblfinlem2  32022  dfrcl4  36312  iunrelexp0  36338  comptiunov2i  36342  corclrcl  36343  trclfvdecomr  36364  dfrtrcl4  36374  corcltrcl  36375  cotrclrcl  36378  fiiuncl  37443  iunp1  37444  sge0iunmptlemfi  38292  iunxprg  39043