Theorem 0iun 5029

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  ∃wrex 3091  ∅c0 4286  ∪ ciun 4958

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-v 3459  df-dif 3909  df-nul 4287  df-iun 4960

This theorem is used by:  iinvdif  5048  iununi  5067  iunopeqop  5506  iunfi  9307  pwsdompw  10202  fsum2d  15847  fsumiun  15898  fprod2d  16060  prmreclem4  17003  prmreclem5  17004  fiuncmp  23613  ovolfiniun  25713  ovoliunnul  25719  finiunmbl  25756  volfiniun  25759  volsup  25768  gsumpart  33449  esum2dlem  34548  sigapildsyslem  34618  fiunelros  34631  mrsubvrs  36053  0totbnd  38484  totbndbnd  38500  fiiuncl  45845  sge0iunmptlemfi  47187  caragenfiiuncl  47289  carageniuncllem1  47295