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

Syntax hints:   = wceq 1542   ∈ wcel 2114  ∃wrex 3062  ∅c0 4287  ∪ ciun 4948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-v 3444  df-dif 3906  df-nul 4288  df-iun 4950

This theorem is referenced by:  iinvdif  5037  iununi  5056  iunfi  9255  pwsdompw  10125  fsum2d  15706  fsumiun  15756  fprod2d  15916  prmreclem4  16859  prmreclem5  16860  fiuncmp  23363  ovolfiniun  25473  ovoliunnul  25479  finiunmbl  25516  volfiniun  25519  volsup  25528  gsumpart  33161  esum2dlem  34274  sigapildsyslem  34343  fiunelros  34356  mrsubvrs  35742  0totbnd  38028  totbndbnd  38044  fiiuncl  45429  sge0iunmptlemfi  46775  caragenfiiuncl  46877  carageniuncllem1  46883