Theorem uni0 4939

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

Assertion

Ref	Expression
uni0	⊢ ∪ ∅ = ∅

Proof of Theorem uni0

Step	Hyp	Ref	Expression
1		0ss 4405	. 2 ⊢ ∅ ⊆ {∅}
2		uni0b 4937	. 2 ⊢ (∪ ∅ = ∅ ↔ ∅ ⊆ {∅})
3	1, 2	mpbir 231	1 ⊢ ∪ ∅ = ∅

Syntax hints:   = wceq 1536   ⊆ wss 3962  ∅c0 4338  {csn 4630  ∪ cuni 4911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-11 2154  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-v 3479  df-dif 3965  df-ss 3979  df-nul 4339  df-sn 4631  df-uni 4912

This theorem is referenced by:  csbuni  4940  uniintsn  4989  iununi  5103  unisn2  5317  eqsnuniex  5366  opswap  6250  unixp0  6304  unixpid  6305  unizlim  6508  iotanul  6540  funfv  6995  dffv2  7003  1stval  8014  2ndval  8015  1stnpr  8016  2ndnpr  8017  1st0  8018  2nd0  8019  1st2val  8040  2nd2val  8041  brtpos0  8256  tpostpos  8269  nnunifi  9324  supval2  9492  sup00  9501  infeq5  9674  rankuni  9900  rankxplim3  9918  iunfictbso  10151  cflim2  10300  fin1a2lem11  10447  itunisuc  10456  itunitc  10458  ttukeylem4  10549  relexpfldd  15085  incexclem  15868  arwval  18096  dprdsn  20070  zrhval  21535  0opn  22925  indistopon  23023  mretopd  23115  hauscmplem  23429  cmpfi  23431  comppfsc  23555  alexsublem  24067  alexsubALTlem2  24071  ptcmplem2  24076  lebnumlem3  25008  old0  27912  made0  27926  locfinref  33801  prsiga  34111  sigapildsys  34142  dya2iocuni  34264  fiunelcarsg  34297  carsgclctunlem1  34298  carsgclctunlem3  34301  wevgblacfn  35092  nnuni  35706  unisnif  35906  limsucncmpi  36427  heicant  37641  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  mbfresfi  37652  onov0suclim  43263  stoweidlem35  45990  stoweidlem39  45994  prsal  46273  issalnnd  46300  ismeannd  46422  caragenunicl  46479  isomennd  46486  ipolub0  48780