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

Theorem 0iun 4387
 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

Proof of Theorem 0iun
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 rex0 3799 . . . 4
2 eliun 4335 . . . 4
31, 2mtbir 299 . . 3
4 noel 3788 . . 3
53, 42false 350 . 2
65eqriv 2453 1
 Colors of variables: wff setvar class Syntax hints:  =wceq 1395  e.wcel 1818  E.wrex 2808   c0 3784  U_ciun 4330 This theorem is referenced by:  iinvdif  4402  iununi  4415  iunfi  7828  pwsdompw  8605  fsum2d  13586  fsumiun  13635  fprod2d  13785  prmreclem4  14437  prmreclem5  14438  fiuncmp  19904  ovolfiniun  21912  ovoliunnul  21918  finiunmbl  21954  volfiniun  21957  volsup  21966  mrsubvrs  28882  0totbnd  30269  totbndbnd  30285 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111  df-dif 3478  df-nul 3785  df-iun 4332
 Copyright terms: Public domain W3C validator