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

Theorem iun0 4710
Description: An indexed union of the empty set is empty. (Contributed by NM, 26-Mar-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
iun0 𝑥𝐴 ∅ = ∅

Proof of Theorem iun0
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 noel 4067 . . . . 5 ¬ 𝑦 ∈ ∅
21a1i 11 . . . 4 (𝑥𝐴 → ¬ 𝑦 ∈ ∅)
32nrex 3148 . . 3 ¬ ∃𝑥𝐴 𝑦 ∈ ∅
4 eliun 4658 . . 3 (𝑦 𝑥𝐴 ∅ ↔ ∃𝑥𝐴 𝑦 ∈ ∅)
53, 4mtbir 312 . 2 ¬ 𝑦 𝑥𝐴
65nel0 4079 1 𝑥𝐴 ∅ = ∅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1631  wcel 2145  wrex 3062  c0 4063   ciun 4654
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-v 3353  df-dif 3726  df-nul 4064  df-iun 4656
This theorem is referenced by:  iunxdif3  4740  iununi  4744  funiunfv  6649  om0r  7773  kmlem11  9184  ituniiun  9446  voliunlem1  23538  ofpreima2  29806  esum2dlem  30494  sigaclfu2  30524  measvunilem0  30616  measvuni  30617  cvmscld  31593  trpred0  32072  ovolval4lem1  41383
  Copyright terms: Public domain W3C validator