Theorem iun0 5085

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 4360	. . . . 5 ⊢ ¬ 𝑦 ∈ ∅
2	1	a1i 11	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ¬ 𝑦 ∈ ∅)
3	2	nrex 3080	. . 3 ⊢ ¬ ∃𝑥 ∈ 𝐴 𝑦 ∈ ∅
4		eliun 5019	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ∅ ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ ∅)
5	3, 4	mtbir 323	. 2 ⊢ ¬ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ∅
6	5	nel0 4377	1 ⊢ ∪ 𝑥 ∈ 𝐴 ∅ = ∅

Syntax hints:  ¬ wn 3   = wceq 1537   ∈ wcel 2108  ∃wrex 3076  ∅c0 4352  ∪ ciun 5015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-v 3490  df-dif 3979  df-nul 4353  df-iun 5017

This theorem is referenced by:  iunxdif3  5118  iununi  5122  funiunfv  7285  om0r  8595  kmlem11  10230  ituniiun  10491  dfrtrclrec2  15107  voliunlem1  25604  ofpreima2  32684  ssdifidllem  33449  esum2dlem  34056  sigaclfu2  34085  measvunilem0  34177  measvuni  34178  cvmscld  35241  ovolval4lem1  46570