Theorem uni0 4899

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 5261. (Revised by Eric Schmidt, 4-Apr-2007.)

Assertion

Ref	Expression
uni0	⊢ ∪ ∅ = ∅

Proof of Theorem uni0

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

Syntax hints:   = wceq 1540   ⊆ wss 3914  ∅c0 4296  {csn 4589  ∪ cuni 4871

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 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-v 3449  df-dif 3917  df-ss 3931  df-nul 4297  df-sn 4590  df-uni 4872

This theorem is referenced by:  csbuni  4900  uniintsn  4949  iununi  5063  unisn2  5267  eqsnuniex  5316  opswap  6202  unixp0  6256  unixpid  6257  unizlim  6457  iotanul  6489  funfv  6948  dffv2  6956  1stval  7970  2ndval  7971  1stnpr  7972  2ndnpr  7973  1st0  7974  2nd0  7975  1st2val  7996  2nd2val  7997  brtpos0  8212  tpostpos  8225  nnunifi  9238  supval2  9406  sup00  9416  infeq5  9590  rankuni  9816  rankxplim3  9834  iunfictbso  10067  cflim2  10216  fin1a2lem11  10363  itunisuc  10372  itunitc  10374  ttukeylem4  10465  relexpfldd  15016  incexclem  15802  arwval  18005  dprdsn  19968  zrhval  21417  0opn  22791  indistopon  22888  mretopd  22979  hauscmplem  23293  cmpfi  23295  comppfsc  23419  alexsublem  23931  alexsubALTlem2  23935  ptcmplem2  23940  lebnumlem3  24862  old0  27767  made0  27785  locfinref  33831  prsiga  34121  sigapildsys  34152  dya2iocuni  34274  fiunelcarsg  34307  carsgclctunlem1  34308  carsgclctunlem3  34311  wevgblacfn  35096  nnuni  35714  unisnif  35913  limsucncmpi  36433  heicant  37649  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  mbfresfi  37660  onov0suclim  43263  stoweidlem35  46033  stoweidlem39  46037  prsal  46316  issalnnd  46343  ismeannd  46465  caragenunicl  46522  isomennd  46529  dftpos5  48862  ipolub0  48980