Theorem 0iun 5030

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∃wrex 3054  ∅c0 4299  ∪ ciun 4958

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-v 3452  df-dif 3920  df-nul 4300  df-iun 4960

This theorem is referenced by:  iinvdif  5047  iununi  5066  iunfi  9301  pwsdompw  10163  fsum2d  15744  fsumiun  15794  fprod2d  15954  prmreclem4  16897  prmreclem5  16898  fiuncmp  23298  ovolfiniun  25409  ovoliunnul  25415  finiunmbl  25452  volfiniun  25455  volsup  25464  gsumpart  33004  esum2dlem  34089  sigapildsyslem  34158  fiunelros  34171  mrsubvrs  35516  0totbnd  37774  totbndbnd  37790  fiiuncl  45066  sge0iunmptlemfi  46418  caragenfiiuncl  46520  carageniuncllem1  46526