Theorem 0iun 5027

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

Syntax hints:   = wceq 1570   ∈ wcel 2143  ∃wrex 3089  ∅c0 4286  ∪ ciun 4956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-v 3457  df-dif 3908  df-nul 4287  df-iun 4958

This theorem is referenced by:  iinvdif  5046  iununi  5065  iunopeqop  5504  iunfi  9296  pwsdompw  10182  fsum2d  15818  fsumiun  15869  fprod2d  16031  prmreclem4  16974  prmreclem5  16975  fiuncmp  23561  ovolfiniun  25660  ovoliunnul  25666  finiunmbl  25703  volfiniun  25706  volsup  25715  gsumpart  33383  esum2dlem  34482  sigapildsyslem  34551  fiunelros  34564  mrsubvrs  36014  0totbnd  38444  totbndbnd  38460  fiiuncl  45805  sge0iunmptlemfi  47147  caragenfiiuncl  47249  carageniuncllem1  47255