Theorem 0iun 5039

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  ∃wrex 3060  ∅c0 4308  ∪ ciun 4967

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-v 3461  df-dif 3929  df-nul 4309  df-iun 4969

This theorem is referenced by:  iinvdif  5056  iununi  5075  iunfi  9353  pwsdompw  10215  fsum2d  15785  fsumiun  15835  fprod2d  15995  prmreclem4  16937  prmreclem5  16938  fiuncmp  23340  ovolfiniun  25452  ovoliunnul  25458  finiunmbl  25495  volfiniun  25498  volsup  25507  gsumpart  32997  esum2dlem  34069  sigapildsyslem  34138  fiunelros  34151  mrsubvrs  35490  0totbnd  37743  totbndbnd  37759  fiiuncl  45037  sge0iunmptlemfi  46390  caragenfiiuncl  46492  carageniuncllem1  46498