Theorem 0iun 5021

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  ∃wrex 3087  ∅c0 4279  ∪ ciun 4951

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-v 3453  df-dif 3902  df-nul 4280  df-iun 4953

This theorem is used by:  iinvdif  5040  iununi  5059  iunopeqop  5494  iunfi  9332  pwsdompw  10281  fsum2d  15937  fsumiun  15988  fprod2d  16148  prmreclem4  17097  prmreclem5  17098  fiuncmp  23722  ovolfiniun  25822  ovoliunnul  25828  finiunmbl  25865  volfiniun  25868  volsup  25877  gsumpart  33624  esum2dlem  34724  sigapildsyslem  34794  fiunelros  34807  mrsubvrs  36287  0totbnd  38707  totbndbnd  38723  fiiuncl  46081  sge0iunmptlemfi  47422  caragenfiiuncl  47524  carageniuncllem1  47530