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

Theorem iun0 5062
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 4338 . . . . 5 ¬ 𝑦 ∈ ∅
21a1i 11 . . . 4 (𝑥𝐴 → ¬ 𝑦 ∈ ∅)
32nrex 3074 . . 3 ¬ ∃𝑥𝐴 𝑦 ∈ ∅
4 eliun 4995 . . 3 (𝑦 𝑥𝐴 ∅ ↔ ∃𝑥𝐴 𝑦 ∈ ∅)
53, 4mtbir 323 . 2 ¬ 𝑦 𝑥𝐴
65nel0 4354 1 𝑥𝐴 ∅ = ∅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1540  wcel 2108  wrex 3070  c0 4333   ciun 4991
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-v 3482  df-dif 3954  df-nul 4334  df-iun 4993
This theorem is referenced by:  iunxdif3  5095  iununi  5099  funiunfv  7268  om0r  8577  kmlem11  10201  ituniiun  10462  dfrtrclrec2  15097  voliunlem1  25585  ofpreima2  32676  ssdifidllem  33484  esum2dlem  34093  sigaclfu2  34122  measvunilem0  34214  measvuni  34215  cvmscld  35278  ovolval4lem1  46664
  Copyright terms: Public domain W3C validator