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

Theorem iun0 5058
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 4326 . . . . 5 ¬ 𝑦 ∈ ∅
21a1i 11 . . . 4 (𝑥𝐴 → ¬ 𝑦 ∈ ∅)
32nrex 3073 . . 3 ¬ ∃𝑥𝐴 𝑦 ∈ ∅
4 eliun 4994 . . 3 (𝑦 𝑥𝐴 ∅ ↔ ∃𝑥𝐴 𝑦 ∈ ∅)
53, 4mtbir 322 . 2 ¬ 𝑦 𝑥𝐴
65nel0 4346 1 𝑥𝐴 ∅ = ∅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1541  wcel 2106  wrex 3069  c0 4318   ciun 4990
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-v 3475  df-dif 3947  df-nul 4319  df-iun 4992
This theorem is referenced by:  iunxdif3  5091  iununi  5095  funiunfv  7231  om0r  8521  kmlem11  10137  ituniiun  10399  dfrtrclrec2  14987  voliunlem1  24996  ofpreima2  31760  esum2dlem  32921  sigaclfu2  32950  measvunilem0  33042  measvuni  33043  cvmscld  34095  ovolval4lem1  45138
  Copyright terms: Public domain W3C validator