Theorem 0iun 4988

Description: An empty indexed union is empty. (Contributed by NM, 4-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)

Assertion

Ref	Expression
0iun	⊢ ∪ 𝑥 ∈ ∅ 𝐴 = ∅

Proof of Theorem 0iun

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rex0 4319	. . 3 ⊢ ¬ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴
2		eliun 4925	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴 ↔ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴)
3	1, 2	mtbir 325	. 2 ⊢ ¬ 𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴
4	3	nel0 4313	1 ⊢ ∪ 𝑥 ∈ ∅ 𝐴 = ∅

Syntax hints:   = wceq 1537   ∈ wcel 2114  ∃wrex 3141  ∅c0 4293  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-v 3498  df-dif 3941  df-nul 4294  df-iun 4923

This theorem is referenced by:  iinvdif  5004  iununi  5023  iunfi  8814  pwsdompw  9628  fsum2d  15128  fsumiun  15178  fprod2d  15337  prmreclem4  16257  prmreclem5  16258  fiuncmp  22014  ovolfiniun  24104  ovoliunnul  24110  finiunmbl  24147  volfiniun  24150  volsup  24159  esum2dlem  31353  sigapildsyslem  31422  fiunelros  31435  mrsubvrs  32771  0totbnd  35053  totbndbnd  35069  fiiuncl  41334  sge0iunmptlemfi  42702  caragenfiiuncl  42804  carageniuncllem1  42810