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

Theorem 0iun 3959
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 3468 . . . 4  |-  -.  E. x  e.  (/)  y  e.  A
2 eliun 3909 . . . 4  |-  ( y  e.  U_ x  e.  (/)  A  <->  E. x  e.  (/)  y  e.  A )
31, 2mtbir 290 . . 3  |-  -.  y  e.  U_ x  e.  (/)  A
4 noel 3459 . . 3  |-  -.  y  e.  (/)
53, 42false 339 . 2  |-  ( y  e.  U_ x  e.  (/)  A  <->  y  e.  (/) )
65eqriv 2280 1  |-  U_ x  e.  (/)  A  =  (/)
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1684   E.wrex 2544   (/)c0 3455   U_ciun 3905
This theorem is referenced by:  iununi  3986  iunfi  7144  pwsdompw  7830  fsum2d  12234  fsumiun  12279  prmreclem4  12966  prmreclem5  12967  fiuncmp  17131  ovolfiniun  18860  ovoliunnul  18866  finiunmbl  18901  volfiniun  18904  volsup  18913  0totbnd  26497  totbndbnd  26513
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-v 2790  df-dif 3155  df-nul 3456  df-iun 3907
  Copyright terms: Public domain W3C validator