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

Theorem 0iun 4548
 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 3919 . . 3 ¬ ∃𝑥 ∈ ∅ 𝑦𝐴
2 eliun 4495 . . 3 (𝑦 𝑥 ∈ ∅ 𝐴 ↔ ∃𝑥 ∈ ∅ 𝑦𝐴)
31, 2mtbir 313 . 2 ¬ 𝑦 𝑥 ∈ ∅ 𝐴
43nel0 3913 1 𝑥 ∈ ∅ 𝐴 = ∅
 Colors of variables: wff setvar class Syntax hints:   = wceq 1480   ∈ wcel 1987  ∃wrex 2908  ∅c0 3896  ∪ ciun 4490 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-v 3191  df-dif 3562  df-nul 3897  df-iun 4492 This theorem is referenced by:  iinvdif  4563  iununi  4581  iunfi  8206  pwsdompw  8978  fsum2d  14441  fsumiun  14491  fprod2d  14647  prmreclem4  15558  prmreclem5  15559  fiuncmp  21130  ovolfiniun  23192  ovoliunnul  23198  finiunmbl  23235  volfiniun  23238  volsup  23247  esum2dlem  29959  sigapildsyslem  30029  fiunelros  30042  mrsubvrs  31162  0totbnd  33239  totbndbnd  33255  fiiuncl  38752  sge0iunmptlemfi  39963  caragenfiiuncl  40062  carageniuncllem1  40068
 Copyright terms: Public domain W3C validator