Theorem 0iun 5027

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∃wrex 3053  ∅c0 4296  ∪ ciun 4955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-v 3449  df-dif 3917  df-nul 4297  df-iun 4957

This theorem is referenced by:  iinvdif  5044  iununi  5063  iunfi  9294  pwsdompw  10156  fsum2d  15737  fsumiun  15787  fprod2d  15947  prmreclem4  16890  prmreclem5  16891  fiuncmp  23291  ovolfiniun  25402  ovoliunnul  25408  finiunmbl  25445  volfiniun  25448  volsup  25457  gsumpart  32997  esum2dlem  34082  sigapildsyslem  34151  fiunelros  34164  mrsubvrs  35509  0totbnd  37767  totbndbnd  37783  fiiuncl  45059  sge0iunmptlemfi  46411  caragenfiiuncl  46513  carageniuncllem1  46519