Theorem uni0 4911

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

Assertion

Ref	Expression
uni0	⊢ ∪ ∅ = ∅

Proof of Theorem uni0

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

Syntax hints:   = wceq 1540   ⊆ wss 3926  ∅c0 4308  {csn 4601  ∪ cuni 4883

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 2007  ax-8 2110  ax-9 2118  ax-11 2157  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-v 3461  df-dif 3929  df-ss 3943  df-nul 4309  df-sn 4602  df-uni 4884

This theorem is referenced by:  csbuni  4912  uniintsn  4961  iununi  5075  unisn2  5282  eqsnuniex  5331  opswap  6218  unixp0  6272  unixpid  6273  unizlim  6476  iotanul  6508  funfv  6965  dffv2  6973  1stval  7988  2ndval  7989  1stnpr  7990  2ndnpr  7991  1st0  7992  2nd0  7993  1st2val  8014  2nd2val  8015  brtpos0  8230  tpostpos  8243  nnunifi  9297  supval2  9465  sup00  9475  infeq5  9649  rankuni  9875  rankxplim3  9893  iunfictbso  10126  cflim2  10275  fin1a2lem11  10422  itunisuc  10431  itunitc  10433  ttukeylem4  10524  relexpfldd  15067  incexclem  15850  arwval  18054  dprdsn  20017  zrhval  21466  0opn  22840  indistopon  22937  mretopd  23028  hauscmplem  23342  cmpfi  23344  comppfsc  23468  alexsublem  23980  alexsubALTlem2  23984  ptcmplem2  23989  lebnumlem3  24911  old0  27815  made0  27829  locfinref  33818  prsiga  34108  sigapildsys  34139  dya2iocuni  34261  fiunelcarsg  34294  carsgclctunlem1  34295  carsgclctunlem3  34298  wevgblacfn  35077  nnuni  35690  unisnif  35889  limsucncmpi  36409  heicant  37625  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  mbfresfi  37636  onov0suclim  43245  stoweidlem35  46012  stoweidlem39  46016  prsal  46295  issalnnd  46322  ismeannd  46444  caragenunicl  46501  isomennd  46508  dftpos5  48797  ipolub0  48914