Theorem 0iun 5026

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  ∃wrex 3090  ∅c0 4281  ∪ ciun 4956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-v 3456  df-dif 4050  df-nul 4282  df-iun 4958

This theorem is used by:  iinvdif  5045  iununi  5064  iunopeqop  5501  iunfi  9370  pwsdompw  10320  fsum2d  15981  fsumiun  16032  fprod2d  16192  prmreclem4  17141  prmreclem5  17142  fiuncmp  23777  ovolfiniun  25877  ovoliunnul  25883  finiunmbl  25920  volfiniun  25923  volsup  25932  gsumpart  33723  esum2dlem  34835  sigapildsyslem  34905  fiunelros  34918  mrsubvrs  36495  0totbnd  38973  totbndbnd  38989  fiiuncl  46356  sge0iunmptlemfi  47696  caragenfiiuncl  47798  carageniuncllem1  47804