Theorem 0iun 4577

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	|- U_ x e. (/) A = (/)

Proof of Theorem 0iun

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rex0 3938	. . 3 |- -. E. x e. (/) y e. A
2		eliun 4524	. . 3 |- ( y e. U_ x e. (/) A <-> E. x e. (/) y e. A )
3	1, 2	mtbir 313	. 2 |- -. y e. U_ x e. (/) A
4	3	nel0 3932	1 |- U_ x e. (/) A = (/)

Syntax hints:   = wceq 1483   e. wcel 1990   E.wrex 2913   (/)c0 3915   U_ciun 4520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-dif 3577  df-nul 3916  df-iun 4522

This theorem is referenced by:  iinvdif  4592  iununi  4610  iunfi  8254  pwsdompw  9026  fsum2d  14502  fsumiun  14553  fprod2d  14711  prmreclem4  15623  prmreclem5  15624  fiuncmp  21207  ovolfiniun  23269  ovoliunnul  23275  finiunmbl  23312  volfiniun  23315  volsup  23324  esum2dlem  30154  sigapildsyslem  30224  fiunelros  30237  mrsubvrs  31419  0totbnd  33572  totbndbnd  33588  fiiuncl  39234  sge0iunmptlemfi  40630  caragenfiiuncl  40729  carageniuncllem1  40735