Theorem 0iun 4810

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 4166	. . 3 ⊢ ¬ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴
2		eliun 4757	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴 ↔ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴)
3	1, 2	mtbir 315	. 2 ⊢ ¬ 𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴
4	3	nel0 4160	1 ⊢ ∪ 𝑥 ∈ ∅ 𝐴 = ∅

Syntax hints:   = wceq 1601   ∈ wcel 2107  ∃wrex 3091  ∅c0 4141  ∪ ciun 4753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-v 3400  df-dif 3795  df-nul 4142  df-iun 4755

This theorem is referenced by:  iinvdif  4825  iununi  4844  iunfi  8542  pwsdompw  9361  fsum2d  14907  fsumiun  14957  fprod2d  15114  prmreclem4  16027  prmreclem5  16028  fiuncmp  21616  ovolfiniun  23705  ovoliunnul  23711  finiunmbl  23748  volfiniun  23751  volsup  23760  esum2dlem  30752  sigapildsyslem  30822  fiunelros  30835  mrsubvrs  32018  0totbnd  34196  totbndbnd  34212  fiiuncl  40165  sge0iunmptlemfi  41554  caragenfiiuncl  41656  carageniuncllem1  41662