Theorem iun0 5038

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

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2108  ∃wrex 3060  ∅c0 4308  ∪ ciun 4967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-v 3461  df-dif 3929  df-nul 4309  df-iun 4969

This theorem is referenced by:  iunxdif3  5071  iununi  5075  funiunfv  7239  om0r  8549  kmlem11  10173  ituniiun  10434  dfrtrclrec2  15075  voliunlem1  25501  ofpreima2  32590  ssdifidllem  33417  esum2dlem  34069  sigaclfu2  34098  measvunilem0  34190  measvuni  34191  cvmscld  35241  ovolval4lem1  46626