MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iunxun Structured version   Unicode version

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.
StepHypRef 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 )
42, 3orbi12i 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 ) )
51, 4bitr4i 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
) )
85, 6, 73bitr4i 277 . 2  |-  ( y  e.  U_ x  e.  ( A  u.  B
) C  <->  y  e.  ( U_ x  e.  A  C  u.  U_ x  e.  B  C ) )
98eqriv 2450 1  |-  U_ x  e.  ( A  u.  B
) C  =  (
U_ x  e.  A  C  u.  U_ x  e.  B  C )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator