Theorem 0iun 5016

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  ∃wrex 3058  ∅c0 4283  ∪ ciun 4944

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 2706

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 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-v 3440  df-dif 3902  df-nul 4284  df-iun 4946

This theorem is referenced by:  iinvdif  5033  iununi  5052  iunfi  9241  pwsdompw  10111  fsum2d  15692  fsumiun  15742  fprod2d  15902  prmreclem4  16845  prmreclem5  16846  fiuncmp  23346  ovolfiniun  25456  ovoliunnul  25462  finiunmbl  25499  volfiniun  25502  volsup  25511  gsumpart  33095  esum2dlem  34198  sigapildsyslem  34267  fiunelros  34280  mrsubvrs  35665  0totbnd  37913  totbndbnd  37929  fiiuncl  45252  sge0iunmptlemfi  46599  caragenfiiuncl  46701  carageniuncllem1  46707