Theorem uni0 4866

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

Assertion

Ref	Expression
uni0	⊢ ∪ ∅ = ∅

Proof of Theorem uni0

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

Syntax hints:   = wceq 1539   ⊆ wss 3883  ∅c0 4253  {csn 4558  ∪ cuni 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-11 2156  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900  df-nul 4254  df-sn 4559  df-uni 4837

This theorem is referenced by:  csbuni  4867  uniintsn  4915  iununi  5024  unisn2  5231  eqsnuniex  5278  opswap  6121  unixp0  6175  unixpid  6176  unizlim  6368  iotanul  6396  funfv  6837  dffv2  6845  1stval  7806  2ndval  7807  1stnpr  7808  2ndnpr  7809  1st0  7810  2nd0  7811  1st2val  7832  2nd2val  7833  brtpos0  8020  tpostpos  8033  nnunifi  8995  supval2  9144  sup00  9153  infeq5  9325  rankuni  9552  rankxplim3  9570  iunfictbso  9801  cflim2  9950  fin1a2lem11  10097  itunisuc  10106  itunitc  10108  ttukeylem4  10199  relexpfldd  14689  incexclem  15476  arwval  17674  dprdsn  19554  zrhval  20621  0opn  21961  indistopon  22059  mretopd  22151  hauscmplem  22465  cmpfi  22467  comppfsc  22591  alexsublem  23103  alexsubALTlem2  23107  ptcmplem2  23112  lebnumlem3  24032  locfinref  31693  prsiga  31999  sigapildsys  32030  dya2iocuni  32150  fiunelcarsg  32183  carsgclctunlem1  32184  carsgclctunlem3  32187  nnuni  33595  old0  33970  made0  33984  unisnif  34154  limsucncmpi  34561  heicant  35739  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  mbfresfi  35750  stoweidlem35  43466  stoweidlem39  43470  prsal  43749  issalnnd  43774  ismeannd  43895  caragenunicl  43952  isomennd  43959  ipolub0  46166