Theorem iun0 5025

Description: An indexed union of the empty set is empty. (Contributed by NM, 26-Mar-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)

Assertion

Ref	Expression
iun0	⊢ ∪ 𝑥 ∈ 𝐴 ∅ = ∅

Proof of Theorem iun0

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		noel 4290	. . . . 5 ⊢ ¬ 𝑦 ∈ ∅
2	1	a1i 11	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ¬ 𝑦 ∈ ∅)
3	2	nrex 3091	. . 3 ⊢ ¬ ∃𝑥 ∈ 𝐴 𝑦 ∈ ∅
4		eliun 4959	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ∅ ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ ∅)
5	3, 4	mtbir 326	. 2 ⊢ ¬ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ∅
6	5	nel0 4308	1 ⊢ ∪ 𝑥 ∈ 𝐴 ∅ = ∅

Syntax hints:  ¬ wn 3   = wceq 1568   ∈ wcel 2141  ∃wrex 3087  ∅c0 4285  ∪ ciun 4955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-v 3455  df-dif 3907  df-nul 4286  df-iun 4957

This theorem is referenced by:  iunxdif3  5060  iununi  5064  funiunfv  7246  om0r  8523  kmlem11  10143  ituniiun  10405  dfrtrclrec2  15094  ssdifidllem  21463  voliunlem1  25688  ofpreima2  32977  esum2dlem  34448  sigaclfu2  34477  measvunilem0  34569  measvuni  34570  cvmscld  35719  ovolval4lem1  47311