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

Theorem 0iun 4359
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 3782 . . . 4  |-  -.  E. x  e.  (/)  y  e.  A
2 eliun 4307 . . . 4  |-  ( y  e.  U_ x  e.  (/)  A  <->  E. x  e.  (/)  y  e.  A )
31, 2mtbir 300 . . 3  |-  -.  y  e.  U_ x  e.  (/)  A
4 noel 3771 . . 3  |-  -.  y  e.  (/)
53, 42false 351 . 2  |-  ( y  e.  U_ x  e.  (/)  A  <->  y  e.  (/) )
65eqriv 2425 1  |-  U_ x  e.  (/)  A  =  (/)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    e. wcel 1870   E.wrex 2783   (/)c0 3767   U_ciun 4302
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ral 2787  df-rex 2788  df-v 3089  df-dif 3445  df-nul 3768  df-iun 4304
This theorem is referenced by:  iinvdif  4374  iununi  4390  iunfi  7868  pwsdompw  8632  fsum2d  13810  fsumiun  13859  fprod2d  14013  prmreclem4  14826  prmreclem5  14827  fiuncmp  20350  ovolfiniun  22332  ovoliunnul  22338  finiunmbl  22374  volfiniun  22377  volsup  22386  esum2dlem  28752  sigapildsyslem  28822  fiunelros  28835  mrsubvrs  29948  0totbnd  31808  totbndbnd  31824  fiiuncl  37047  sge0iunmptlemfi  37788  caragenfiiuncl  37844  carageniuncllem1  37850
  Copyright terms: Public domain W3C validator