Theorem 0iun 4513

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 3894	. . . 4 ⊢ ¬ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴
2		eliun 4460	. . . 4 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴 ↔ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴)
3	1, 2	mtbir 312	. . 3 ⊢ ¬ 𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴
4		noel 3878	. . 3 ⊢ ¬ 𝑦 ∈ ∅
5	3, 4	2false 364	. 2 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴 ↔ 𝑦 ∈ ∅)
6	5	eqriv 2607	1 ⊢ ∪ 𝑥 ∈ ∅ 𝐴 = ∅

Syntax hints:   = wceq 1475   ∈ wcel 1977  ∃wrex 2897  ∅c0 3874  ∪ ciun 4455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-dif 3543  df-nul 3875  df-iun 4457

This theorem is referenced by:  iinvdif  4528  iununi  4546  iunfi  8137  pwsdompw  8909  fsum2d  14344  fsumiun  14394  fprod2d  14550  prmreclem4  15461  prmreclem5  15462  fiuncmp  21017  ovolfiniun  23076  ovoliunnul  23082  finiunmbl  23119  volfiniun  23122  volsup  23131  esum2dlem  29481  sigapildsyslem  29551  fiunelros  29564  mrsubvrs  30673  0totbnd  32742  totbndbnd  32758  fiiuncl  38259  sge0iunmptlemfi  39306  caragenfiiuncl  39405  carageniuncllem1  39411