Theorem uni0 4889

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

Assertion

Ref	Expression
uni0	⊢ ∪ ∅ = ∅

Proof of Theorem uni0

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

Syntax hints:   = wceq 1540   ⊆ wss 3905  ∅c0 4286  {csn 4579  ∪ cuni 4861

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 3440  df-dif 3908  df-ss 3922  df-nul 4287  df-sn 4580  df-uni 4862

This theorem is referenced by:  csbuni  4890  uniintsn  4938  iununi  5051  unisn2  5254  eqsnuniex  5303  opswap  6182  unixp0  6235  unixpid  6236  unizlim  6435  iotanul  6466  funfv  6914  dffv2  6922  1stval  7933  2ndval  7934  1stnpr  7935  2ndnpr  7936  1st0  7937  2nd0  7938  1st2val  7959  2nd2val  7960  brtpos0  8173  tpostpos  8186  nnunifi  9196  supval2  9364  sup00  9374  infeq5  9552  rankuni  9778  rankxplim3  9796  iunfictbso  10027  cflim2  10176  fin1a2lem11  10323  itunisuc  10332  itunitc  10334  ttukeylem4  10425  relexpfldd  14975  incexclem  15761  arwval  17968  dprdsn  19935  zrhval  21432  0opn  22807  indistopon  22904  mretopd  22995  hauscmplem  23309  cmpfi  23311  comppfsc  23435  alexsublem  23947  alexsubALTlem2  23951  ptcmplem2  23956  lebnumlem3  24878  old0  27787  made0  27805  locfinref  33810  prsiga  34100  sigapildsys  34131  dya2iocuni  34253  fiunelcarsg  34286  carsgclctunlem1  34287  carsgclctunlem3  34290  wevgblacfn  35084  nnuni  35702  unisnif  35901  limsucncmpi  36421  heicant  37637  ovoliunnfl  37644  voliunnfl  37646  volsupnfl  37647  mbfresfi  37648  onov0suclim  43250  stoweidlem35  46020  stoweidlem39  46024  prsal  46303  issalnnd  46330  ismeannd  46452  caragenunicl  46509  isomennd  46516  dftpos5  48862  ipolub0  48980