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

Theorem 0iun 4349
Description: An empty indexed union is empty. (Contributed by NM, 4-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
0iun  |-  U_ x  e.  (/)  A  =  (/)

Proof of Theorem 0iun
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 rex0 3758 . . . 4  |-  -.  E. x  e.  (/)  y  e.  A
2 eliun 4297 . . . 4  |-  ( y  e.  U_ x  e.  (/)  A  <->  E. x  e.  (/)  y  e.  A )
31, 2mtbir 305 . . 3  |-  -.  y  e.  U_ x  e.  (/)  A
4 noel 3747 . . 3  |-  -.  y  e.  (/)
53, 42false 356 . 2  |-  ( y  e.  U_ x  e.  (/)  A  <->  y  e.  (/) )
65eqriv 2459 1  |-  U_ x  e.  (/)  A  =  (/)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1455    e. wcel 1898   E.wrex 2750   (/)c0 3743   U_ciun 4292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754  df-rex 2755  df-v 3059  df-dif 3419  df-nul 3744  df-iun 4294
This theorem is referenced by:  iinvdif  4364  iununi  4380  iunfi  7888  pwsdompw  8660  fsum2d  13881  fsumiun  13930  fprod2d  14084  prmreclem4  14912  prmreclem5  14913  fiuncmp  20468  ovolfiniun  22503  ovoliunnul  22509  finiunmbl  22546  volfiniun  22549  volsup  22558  esum2dlem  28962  sigapildsyslem  29032  fiunelros  29045  mrsubvrs  30209  0totbnd  32150  totbndbnd  32166  fiiuncl  37444  sge0iunmptlemfi  38293  caragenfiiuncl  38374  carageniuncllem1  38380
  Copyright terms: Public domain W3C validator