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 4288	. . 3 ⊢ ¬ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴
2		eliun 4925	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴 ↔ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴)
3	1, 2	mtbir 322	. 2 ⊢ ¬ 𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴
4	3	nel0 4281	1 ⊢ ∪ 𝑥 ∈ ∅ 𝐴 = ∅

Syntax hints:   = wceq 1539   ∈ wcel 2108  ∃wrex 3064  ∅c0 4253  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-v 3424  df-dif 3886  df-nul 4254  df-iun 4923

This theorem is referenced by:  iinvdif  5005  iununi  5024  iunfi  9037  pwsdompw  9891  fsum2d  15411  fsumiun  15461  fprod2d  15619  prmreclem4  16548  prmreclem5  16549  fiuncmp  22463  ovolfiniun  24570  ovoliunnul  24576  finiunmbl  24613  volfiniun  24616  volsup  24625  gsumpart  31217  esum2dlem  31960  sigapildsyslem  32029  fiunelros  32042  mrsubvrs  33384  0totbnd  35858  totbndbnd  35874  fiiuncl  42502  sge0iunmptlemfi  43841  caragenfiiuncl  43943  carageniuncllem1  43949