Theorem 0iun 5018

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  ∃wrex 3060  ∅c0 4285  ∪ ciun 4946

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-v 3442  df-dif 3904  df-nul 4286  df-iun 4948

This theorem is referenced by:  iinvdif  5035  iununi  5054  iunfi  9243  pwsdompw  10113  fsum2d  15694  fsumiun  15744  fprod2d  15904  prmreclem4  16847  prmreclem5  16848  fiuncmp  23348  ovolfiniun  25458  ovoliunnul  25464  finiunmbl  25501  volfiniun  25504  volsup  25513  gsumpart  33146  esum2dlem  34249  sigapildsyslem  34318  fiunelros  34331  mrsubvrs  35716  0totbnd  37974  totbndbnd  37990  fiiuncl  45320  sge0iunmptlemfi  46667  caragenfiiuncl  46769  carageniuncllem1  46775