Theorem 0iun 5023

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 4310	. . 3 ⊢ ¬ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴
2		eliun 4957	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴 ↔ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴)
3	1, 2	mtbir 326	. 2 ⊢ ¬ 𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴
4	3	nel0 4304	1 ⊢ ∪ 𝑥 ∈ ∅ 𝐴 = ∅

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2146  ∃wrex 3089  ∅c0 4280  ∪ ciun 4953

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-v 3455  df-dif 4049  df-nul 4281  df-iun 4955

This theorem is used by:  iinvdif  5042  iununi  5061  iunopeqop  5497  iunfi  9343  pwsdompw  10291  fsum2d  15949  fsumiun  16000  fprod2d  16160  prmreclem4  17109  prmreclem5  17110  fiuncmp  23734  ovolfiniun  25834  ovoliunnul  25840  finiunmbl  25877  volfiniun  25880  volsup  25889  gsumpart  33677  esum2dlem  34777  sigapildsyslem  34847  fiunelros  34860  mrsubvrs  36408  0totbnd  38847  totbndbnd  38863  fiiuncl  46221  sge0iunmptlemfi  47562  caragenfiiuncl  47664  carageniuncllem1  47670