Theorem 0iun 5086

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

Syntax hints:   = wceq 1537   ∈ wcel 2108  ∃wrex 3076  ∅c0 4352  ∪ ciun 5015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-v 3490  df-dif 3979  df-nul 4353  df-iun 5017

This theorem is referenced by:  iinvdif  5103  iununi  5122  iunfi  9411  pwsdompw  10272  fsum2d  15819  fsumiun  15869  fprod2d  16029  prmreclem4  16966  prmreclem5  16967  fiuncmp  23433  ovolfiniun  25555  ovoliunnul  25561  finiunmbl  25598  volfiniun  25601  volsup  25610  gsumpart  33038  esum2dlem  34056  sigapildsyslem  34125  fiunelros  34138  mrsubvrs  35490  0totbnd  37733  totbndbnd  37749  fiiuncl  44967  sge0iunmptlemfi  46334  caragenfiiuncl  46436  carageniuncllem1  46442