Theorem uni0 4869

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

Assertion

Ref	Expression
uni0	⊢ ∪ ∅ = ∅

Proof of Theorem uni0

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

Syntax hints:   = wceq 1539   ⊆ wss 3887  ∅c0 4256  {csn 4561  ∪ cuni 4839

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-v 3434  df-dif 3890  df-in 3894  df-ss 3904  df-nul 4257  df-sn 4562  df-uni 4840

This theorem is referenced by:  csbuni  4870  uniintsn  4918  iununi  5028  unisn2  5236  eqsnuniex  5283  opswap  6132  unixp0  6186  unixpid  6187  unizlim  6383  iotanul  6411  funfv  6855  dffv2  6863  1stval  7833  2ndval  7834  1stnpr  7835  2ndnpr  7836  1st0  7837  2nd0  7838  1st2val  7859  2nd2val  7860  brtpos0  8049  tpostpos  8062  nnunifi  9065  supval2  9214  sup00  9223  infeq5  9395  rankuni  9621  rankxplim3  9639  iunfictbso  9870  cflim2  10019  fin1a2lem11  10166  itunisuc  10175  itunitc  10177  ttukeylem4  10268  relexpfldd  14761  incexclem  15548  arwval  17758  dprdsn  19639  zrhval  20709  0opn  22053  indistopon  22151  mretopd  22243  hauscmplem  22557  cmpfi  22559  comppfsc  22683  alexsublem  23195  alexsubALTlem2  23199  ptcmplem2  23204  lebnumlem3  24126  locfinref  31791  prsiga  32099  sigapildsys  32130  dya2iocuni  32250  fiunelcarsg  32283  carsgclctunlem1  32284  carsgclctunlem3  32287  nnuni  33692  old0  34043  made0  34057  unisnif  34227  limsucncmpi  34634  heicant  35812  ovoliunnfl  35819  voliunnfl  35821  volsupnfl  35822  mbfresfi  35823  stoweidlem35  43576  stoweidlem39  43580  prsal  43859  issalnnd  43884  ismeannd  44005  caragenunicl  44062  isomennd  44069  ipolub0  46278