Theorem 0iun 5022

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

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

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 3446  df-dif 3914  df-nul 4293  df-iun 4953

This theorem is referenced by:  iinvdif  5039  iununi  5058  iunfi  9270  pwsdompw  10132  fsum2d  15713  fsumiun  15763  fprod2d  15923  prmreclem4  16866  prmreclem5  16867  fiuncmp  23324  ovolfiniun  25435  ovoliunnul  25441  finiunmbl  25478  volfiniun  25481  volsup  25490  gsumpart  33040  esum2dlem  34075  sigapildsyslem  34144  fiunelros  34157  mrsubvrs  35502  0totbnd  37760  totbndbnd  37776  fiiuncl  45052  sge0iunmptlemfi  46404  caragenfiiuncl  46506  carageniuncllem1  46512