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

Theorem iun0 4506
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 3877 . . . . . 6 ¬ 𝑦 ∈ ∅
21a1i 11 . . . . 5 (𝑥𝐴 → ¬ 𝑦 ∈ ∅)
32nrex 2982 . . . 4 ¬ ∃𝑥𝐴 𝑦 ∈ ∅
4 eliun 4454 . . . 4 (𝑦 𝑥𝐴 ∅ ↔ ∃𝑥𝐴 𝑦 ∈ ∅)
53, 4mtbir 311 . . 3 ¬ 𝑦 𝑥𝐴
65, 12false 363 . 2 (𝑦 𝑥𝐴 ∅ ↔ 𝑦 ∈ ∅)
76eqriv 2606 1 𝑥𝐴 ∅ = ∅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1474  wcel 1976  wrex 2896  c0 3873   ciun 4449
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-v 3174  df-dif 3542  df-nul 3874  df-iun 4451
This theorem is referenced by:  iunxdif3  4536  iununi  4540  funiunfv  6387  om0r  7483  kmlem11  8842  ituniiun  9104  voliunlem1  23069  ofpreima2  28642  esum2dlem  29274  sigaclfu2  29304  measvunilem0  29396  measvuni  29397  cvmscld  30302  trpred0  30773  ovolval4lem1  39322
  Copyright terms: Public domain W3C validator