Theorem 0iun 5005

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  ∃wrex 3061  ∅c0 4273  ∪ ciun 4933

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-v 3431  df-dif 3892  df-nul 4274  df-iun 4935

This theorem is referenced by:  iinvdif  5022  iununi  5041  iunopeqop  5475  iunfi  9253  pwsdompw  10125  fsum2d  15733  fsumiun  15784  fprod2d  15946  prmreclem4  16890  prmreclem5  16891  fiuncmp  23369  ovolfiniun  25468  ovoliunnul  25474  finiunmbl  25511  volfiniun  25514  volsup  25523  gsumpart  33124  esum2dlem  34236  sigapildsyslem  34305  fiunelros  34318  mrsubvrs  35704  0totbnd  38094  totbndbnd  38110  fiiuncl  45496  sge0iunmptlemfi  46841  caragenfiiuncl  46943  carageniuncllem1  46949