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

Theorem iun0 4953
 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 4232 . . . . 5 ¬ 𝑦 ∈ ∅
21a1i 11 . . . 4 (𝑥𝐴 → ¬ 𝑦 ∈ ∅)
32nrex 3193 . . 3 ¬ ∃𝑥𝐴 𝑦 ∈ ∅
4 eliun 4890 . . 3 (𝑦 𝑥𝐴 ∅ ↔ ∃𝑥𝐴 𝑦 ∈ ∅)
53, 4mtbir 326 . 2 ¬ 𝑦 𝑥𝐴
65nel0 4251 1 𝑥𝐴 ∅ = ∅
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   = wceq 1538   ∈ wcel 2111  ∃wrex 3071  ∅c0 4227  ∪ ciun 4886 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-fal 1551  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ral 3075  df-rex 3076  df-v 3411  df-dif 3863  df-nul 4228  df-iun 4888 This theorem is referenced by:  iunxdif3  4985  iununi  4989  funiunfv  7004  om0r  8179  kmlem11  9625  ituniiun  9887  dfrtrclrec2  14470  voliunlem1  24255  ofpreima2  30531  esum2dlem  31583  sigaclfu2  31612  measvunilem0  31704  measvuni  31705  cvmscld  32755  trpred0  33326  ovolval4lem1  43682
 Copyright terms: Public domain W3C validator