Theorem iunxun 4400

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 3670	. . . 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 4320	. . . . 5 |- ( y e. U_ x e. A C <-> E. x e. A y e. C )
3		eliun 4320	. . . . 5 |- ( y e. U_ x e. B C <-> E. x e. B y e. C )
4	2, 3	orbi12i 519	. . . 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 4320	. . 3 |- ( y e. U_ x e. ( A u. B ) C <-> E. x e. ( A u. B ) y e. C )
7		elun 3631	. . 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 2450	1 |- U_ x e. ( A u. B ) C = ( U_ x e. A C u. U_ x e. B C )

Syntax hints:   \/ wo 366   = wceq 1398   e. wcel 1823   E.wrex 2805   u. cun 3459   U_ciun 4315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-rex 2810  df-v 3108  df-un 3466  df-iun 4317

This theorem is referenced by:  iunsuc  4949  funiunfv  6135  iunfi  7800  kmlem11  8531  ackbij1lem9  8599  fsum2dlem  13670  fsumiun  13720  fprod2dlem  13869  prmreclem4  14524  fiuncmp  20074  ovolfiniun  22081  finiunmbl  22123  volfiniun  22126  voliunlem1  22129  uniioombllem4  22164  iunxdif3  27640  iuninc  27641  ofpreima2  27738  indval2  28247  esum2dlem  28324  sigaclfu2  28354  measvuni  28425  cvmliftlem10  29006  mrsubvrs  29149  mblfinlem2  30295  iunxprg  32695  dfrcl4  38218  dfrtrcl4  38236  comptiunov2i  38237  iunrelexp0  38245  corclrcl  38251  corcltrcl  38252  cotrclrcl  38253