Theorem 0iun 4949

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

Syntax hints:   = wceq 1538   ∈ wcel 2111  ∃wrex 3107  ∅c0 4243  ∪ ciun 4881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-dif 3884  df-nul 4244  df-iun 4883

This theorem is referenced by:  iinvdif  4965  iununi  4984  iunfi  8796  pwsdompw  9615  fsum2d  15118  fsumiun  15168  fprod2d  15327  prmreclem4  16245  prmreclem5  16246  fiuncmp  22009  ovolfiniun  24105  ovoliunnul  24111  finiunmbl  24148  volfiniun  24151  volsup  24160  gsumpart  30740  esum2dlem  31461  sigapildsyslem  31530  fiunelros  31543  mrsubvrs  32882  0totbnd  35211  totbndbnd  35227  fiiuncl  41699  sge0iunmptlemfi  43052  caragenfiiuncl  43154  carageniuncllem1  43160