Theorem 0iun 5031

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

Syntax hints:   = wceq 1567   ∈ wcel 2149  ∃wrex 3095  ∅c0 4294  ∪ ciun 4960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-v 3465  df-dif 3916  df-nul 4295  df-iun 4962

This theorem is referenced by:  iinvdif  5050  iununi  5069  iunopeqop  5505  iunfi  9300  pwsdompw  10186  fsum2d  15822  fsumiun  15873  fprod2d  16035  prmreclem4  16979  prmreclem5  16980  fiuncmp  23530  ovolfiniun  25629  ovoliunnul  25635  finiunmbl  25672  volfiniun  25675  volsup  25684  gsumpart  33324  esum2dlem  34427  sigapildsyslem  34496  fiunelros  34509  mrsubvrs  35913  0totbnd  38312  totbndbnd  38328  fiiuncl  45677  sge0iunmptlemfi  47019  caragenfiiuncl  47121  carageniuncllem1  47127