Theorem iun0 5023

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 4286	. . . . 5 ⊢ ¬ 𝑦 ∈ ∅
2	1	a1i 11	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ¬ 𝑦 ∈ ∅)
3	2	nrex 3094	. . 3 ⊢ ¬ ∃𝑥 ∈ 𝐴 𝑦 ∈ ∅
4		eliun 4958	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ∅ ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ ∅)
5	3, 4	mtbir 326	. 2 ⊢ ¬ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ∅
6	5	nel0 4305	1 ⊢ ∪ 𝑥 ∈ 𝐴 ∅ = ∅

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2147  ∃wrex 3090  ∅c0 4281  ∪ ciun 4954

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-v 3456  df-dif 4050  df-nul 4282  df-iun 4956

This theorem is used by:  iunxdif3  5058  iununi  5062  funiunfv  7272  om0r  8572  kmlem11  10263  ituniiun  10524  dfrtrclrec2  15237  ssdifidllem  21667  voliunlem1  25898  ofpreima2  33329  esum2dlem  34791  sigaclfu2  34820  measvunilem0  34913  measvuni  34914  cvmscld  36204  ovolval4lem1  47862