Theorem 0iun 5006

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 4301	. . 3 ⊢ ¬ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴
2		eliun 4938	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴 ↔ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴)
3	1, 2	mtbir 323	. 2 ⊢ ¬ 𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴
4	3	nel0 4295	1 ⊢ ∪ 𝑥 ∈ ∅ 𝐴 = ∅

Syntax hints:   = wceq 1542   ∈ wcel 2114  ∃wrex 3062  ∅c0 4274  ∪ ciun 4934

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-v 3432  df-dif 3893  df-nul 4275  df-iun 4936

This theorem is referenced by:  iinvdif  5023  iununi  5042  iunfi  9247  pwsdompw  10119  fsum2d  15727  fsumiun  15778  fprod2d  15940  prmreclem4  16884  prmreclem5  16885  fiuncmp  23382  ovolfiniun  25481  ovoliunnul  25487  finiunmbl  25524  volfiniun  25527  volsup  25536  gsumpart  33142  esum2dlem  34255  sigapildsyslem  34324  fiunelros  34337  mrsubvrs  35723  0totbnd  38111  totbndbnd  38127  fiiuncl  45517  sge0iunmptlemfi  46862  caragenfiiuncl  46964  carageniuncllem1  46970