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

Theorem 0iun 4810
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 4166 . . 3 ¬ ∃𝑥 ∈ ∅ 𝑦𝐴
2 eliun 4757 . . 3 (𝑦 𝑥 ∈ ∅ 𝐴 ↔ ∃𝑥 ∈ ∅ 𝑦𝐴)
31, 2mtbir 315 . 2 ¬ 𝑦 𝑥 ∈ ∅ 𝐴
43nel0 4160 1 𝑥 ∈ ∅ 𝐴 = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1601  wcel 2107  wrex 3091  c0 4141   ciun 4753
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-v 3400  df-dif 3795  df-nul 4142  df-iun 4755
This theorem is referenced by:  iinvdif  4825  iununi  4844  iunfi  8542  pwsdompw  9361  fsum2d  14907  fsumiun  14957  fprod2d  15114  prmreclem4  16027  prmreclem5  16028  fiuncmp  21616  ovolfiniun  23705  ovoliunnul  23711  finiunmbl  23748  volfiniun  23751  volsup  23760  esum2dlem  30752  sigapildsyslem  30822  fiunelros  30835  mrsubvrs  32018  0totbnd  34196  totbndbnd  34212  fiiuncl  40165  sge0iunmptlemfi  41554  caragenfiiuncl  41656  carageniuncllem1  41662
  Copyright terms: Public domain W3C validator