Theorem 0iun 5020

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 4313	. . 3 ⊢ ¬ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴
2		eliun 4953	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴 ↔ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴)
3	1, 2	mtbir 325	. 2 ⊢ ¬ 𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴
4	3	nel0 4307	1 ⊢ ∪ 𝑥 ∈ ∅ 𝐴 = ∅

Syntax hints:   = wceq 1560   ∈ wcel 2142  ∃wrex 3086  ∅c0 4285  ∪ ciun 4949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-v 3456  df-dif 3907  df-nul 4286  df-iun 4951

This theorem is referenced by:  iinvdif  5037  iununi  5056  iunopeqop  5490  iunfi  9286  pwsdompw  10159  fsum2d  15798  fsumiun  15849  fprod2d  16011  prmreclem4  16955  prmreclem5  16956  fiuncmp  23464  ovolfiniun  25563  ovoliunnul  25569  finiunmbl  25606  volfiniun  25609  volsup  25618  gsumpart  33243  esum2dlem  34389  sigapildsyslem  34458  fiunelros  34471  mrsubvrs  35872  0totbnd  38272  totbndbnd  38288  fiiuncl  45645  sge0iunmptlemfi  46987  caragenfiiuncl  47089  carageniuncllem1  47095