Theorem uni0 4887

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

Assertion

Ref	Expression
uni0	⊢ ∪ ∅ = ∅

Proof of Theorem uni0

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

Syntax hints:   = wceq 1541   ⊆ wss 3902  ∅c0 4283  {csn 4576  ∪ cuni 4859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-11 2160  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-v 3438  df-dif 3905  df-ss 3919  df-nul 4284  df-sn 4577  df-uni 4860

This theorem is referenced by:  csbuni  4888  uniintsn  4935  iununi  5047  unisn2  5250  eqsnuniex  5299  opswap  6176  unixp0  6230  unixpid  6231  unizlim  6430  iotanul  6461  funfv  6909  dffv2  6917  1stval  7923  2ndval  7924  1stnpr  7925  2ndnpr  7926  1st0  7927  2nd0  7928  1st2val  7949  2nd2val  7950  brtpos0  8163  tpostpos  8176  nnunifi  9175  supval2  9339  sup00  9349  infeq5  9527  rankuni  9756  rankxplim3  9774  iunfictbso  10005  cflim2  10154  fin1a2lem11  10301  itunisuc  10310  itunitc  10312  ttukeylem4  10403  relexpfldd  14957  incexclem  15743  arwval  17950  dprdsn  19951  zrhval  21445  0opn  22820  indistopon  22917  mretopd  23008  hauscmplem  23322  cmpfi  23324  comppfsc  23448  alexsublem  23960  alexsubALTlem2  23964  ptcmplem2  23969  lebnumlem3  24890  old0  27801  made0  27819  locfinref  33852  prsiga  34142  sigapildsys  34173  dya2iocuni  34294  fiunelcarsg  34327  carsgclctunlem1  34328  carsgclctunlem3  34331  fissorduni  35099  fineqvnttrclselem1  35139  wevgblacfn  35151  nnuni  35769  unisnif  35965  limsucncmpi  36485  heicant  37701  ovoliunnfl  37708  voliunnfl  37710  volsupnfl  37711  mbfresfi  37712  onov0suclim  43313  stoweidlem35  46079  stoweidlem39  46083  prsal  46362  issalnnd  46389  ismeannd  46511  caragenunicl  46568  isomennd  46575  dftpos5  48911  ipolub0  49029