Theorem 0iun 5012

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

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

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 3438  df-dif 3906  df-nul 4285  df-iun 4943

This theorem is referenced by:  iinvdif  5029  iununi  5048  iunfi  9233  pwsdompw  10097  fsum2d  15678  fsumiun  15728  fprod2d  15888  prmreclem4  16831  prmreclem5  16832  fiuncmp  23289  ovolfiniun  25400  ovoliunnul  25406  finiunmbl  25443  volfiniun  25446  volsup  25455  gsumpart  33011  esum2dlem  34065  sigapildsyslem  34134  fiunelros  34147  mrsubvrs  35505  0totbnd  37763  totbndbnd  37779  fiiuncl  45053  sge0iunmptlemfi  46404  caragenfiiuncl  46506  carageniuncllem1  46512