Theorem uni0 4401

Description: The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul 4717 by Eric Schmidt.) (Contributed by NM, 16-Sep-1993.) (Revised by Eric Schmidt, 4-Apr-2007.)

Assertion

Ref	Expression
uni0	⊢ ∪ ∅ = ∅

Proof of Theorem uni0

Step	Hyp	Ref	Expression
1		0ss 3924	. 2 ⊢ ∅ ⊆ {∅}
2		uni0b 4399	. 2 ⊢ (∪ ∅ = ∅ ↔ ∅ ⊆ {∅})
3	1, 2	mpbir 220	1 ⊢ ∪ ∅ = ∅

Syntax hints:   = wceq 1475   ⊆ wss 3540  ∅c0 3874  {csn 4125  ∪ cuni 4372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554  df-nul 3875  df-sn 4126  df-uni 4373

This theorem is referenced by:  csbuni  4402  uniintsn  4449  iununi  4546  unisn2  4722  opswap  5540  unixp0  5586  unixpid  5587  unizlim  5761  iotanul  5783  funfv  6175  dffv2  6181  1stval  7061  2ndval  7062  1stnpr  7063  2ndnpr  7064  1st0  7065  2nd0  7066  1st2val  7085  2nd2val  7086  brtpos0  7246  tpostpos  7259  nnunifi  8096  supval2  8244  sup00  8253  infeq5  8417  rankuni  8609  rankxplim3  8627  iunfictbso  8820  cflim2  8968  fin1a2lem11  9115  itunisuc  9124  itunitc  9126  ttukeylem4  9217  incexclem  14407  arwval  16516  dprdsn  18258  zrhval  19675  0opn  20534  indistopon  20615  mretopd  20706  hauscmplem  21019  cmpfi  21021  comppfsc  21145  alexsublem  21658  alexsubALTlem2  21662  ptcmplem2  21667  lebnumlem3  22570  locfinref  29236  prsiga  29521  sigapildsys  29552  dya2iocuni  29672  fiunelcarsg  29705  carsgclctunlem1  29706  carsgclctunlem3  29709  unisnif  31202  limsucncmpi  31614  heicant  32614  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  mbfresfi  32626  stoweidlem35  38928  stoweidlem39  38932  prsal  39214  issalnnd  39239  ismeannd  39360  caragenunicl  39414  isomennd  39421