Theorem uni0 4959

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

Assertion

Ref	Expression
uni0	⊢ ∪ ∅ = ∅

Proof of Theorem uni0

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

Syntax hints:   = wceq 1537   ⊆ wss 3976  ∅c0 4352  {csn 4648  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-11 2158  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-v 3490  df-dif 3979  df-ss 3993  df-nul 4353  df-sn 4649  df-uni 4932

This theorem is referenced by:  csbuni  4960  uniintsn  5009  iununi  5122  unisn2  5330  eqsnuniex  5379  opswap  6260  unixp0  6314  unixpid  6315  unizlim  6518  iotanul  6551  funfv  7009  dffv2  7017  1stval  8032  2ndval  8033  1stnpr  8034  2ndnpr  8035  1st0  8036  2nd0  8037  1st2val  8058  2nd2val  8059  brtpos0  8274  tpostpos  8287  nnunifi  9355  supval2  9524  sup00  9533  infeq5  9706  rankuni  9932  rankxplim3  9950  iunfictbso  10183  cflim2  10332  fin1a2lem11  10479  itunisuc  10488  itunitc  10490  ttukeylem4  10581  relexpfldd  15099  incexclem  15884  arwval  18110  dprdsn  20080  zrhval  21541  0opn  22931  indistopon  23029  mretopd  23121  hauscmplem  23435  cmpfi  23437  comppfsc  23561  alexsublem  24073  alexsubALTlem2  24077  ptcmplem2  24082  lebnumlem3  25014  old0  27916  made0  27930  locfinref  33787  prsiga  34095  sigapildsys  34126  dya2iocuni  34248  fiunelcarsg  34281  carsgclctunlem1  34282  carsgclctunlem3  34285  wevgblacfn  35076  nnuni  35689  unisnif  35889  limsucncmpi  36411  heicant  37615  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  mbfresfi  37626  onov0suclim  43236  stoweidlem35  45956  stoweidlem39  45960  prsal  46239  issalnnd  46266  ismeannd  46388  caragenunicl  46445  isomennd  46452  ipolub0  48664