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

Assertion

Ref	Expression
uni0	⊢ ∪ ∅ = ∅

Proof of Theorem uni0

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

Syntax hints:   = wceq 1541   ⊆ wss 3948  ∅c0 4322  {csn 4628  ∪ cuni 4908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-v 3476  df-dif 3951  df-in 3955  df-ss 3965  df-nul 4323  df-sn 4629  df-uni 4909

This theorem is referenced by:  csbuni  4940  uniintsn  4991  iununi  5102  unisn2  5312  eqsnuniex  5359  opswap  6228  unixp0  6282  unixpid  6283  unizlim  6487  iotanul  6521  funfv  6978  dffv2  6986  1stval  7979  2ndval  7980  1stnpr  7981  2ndnpr  7982  1st0  7983  2nd0  7984  1st2val  8005  2nd2val  8006  brtpos0  8220  tpostpos  8233  nnunifi  9296  supval2  9452  sup00  9461  infeq5  9634  rankuni  9860  rankxplim3  9878  iunfictbso  10111  cflim2  10260  fin1a2lem11  10407  itunisuc  10416  itunitc  10418  ttukeylem4  10509  relexpfldd  14999  incexclem  15784  arwval  17995  dprdsn  19908  zrhval  21063  0opn  22413  indistopon  22511  mretopd  22603  hauscmplem  22917  cmpfi  22919  comppfsc  23043  alexsublem  23555  alexsubALTlem2  23559  ptcmplem2  23564  lebnumlem3  24486  old0  27362  made0  27376  locfinref  32890  prsiga  33198  sigapildsys  33229  dya2iocuni  33351  fiunelcarsg  33384  carsgclctunlem1  33385  carsgclctunlem3  33388  nnuni  34771  unisnif  34972  limsucncmpi  35422  heicant  36615  ovoliunnfl  36622  voliunnfl  36624  volsupnfl  36625  mbfresfi  36626  onov0suclim  42112  stoweidlem35  44836  stoweidlem39  44840  prsal  45119  issalnnd  45146  ismeannd  45268  caragenunicl  45325  isomennd  45332  ipolub0  47701