Theorem 0iun 5067

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

Syntax hints:   = wceq 1542   ∈ wcel 2107  ∃wrex 3071  ∅c0 4323  ∪ ciun 4998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-v 3477  df-dif 3952  df-nul 4324  df-iun 5000

This theorem is referenced by:  iinvdif  5084  iununi  5103  iunfi  9340  pwsdompw  10199  fsum2d  15717  fsumiun  15767  fprod2d  15925  prmreclem4  16852  prmreclem5  16853  fiuncmp  22908  ovolfiniun  25018  ovoliunnul  25024  finiunmbl  25061  volfiniun  25064  volsup  25073  gsumpart  32207  esum2dlem  33090  sigapildsyslem  33159  fiunelros  33172  mrsubvrs  34513  0totbnd  36641  totbndbnd  36657  fiiuncl  43752  sge0iunmptlemfi  45129  caragenfiiuncl  45231  carageniuncllem1  45237