Theorem uni0 4887

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

Assertion

Ref	Expression
uni0	⊢ ∪ ∅ = ∅

Proof of Theorem uni0

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

Syntax hints:   = wceq 1541   ⊆ wss 3901  ∅c0 4273  {csn 4577  ∪ cuni 4856

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 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3063  df-rex 3072  df-v 3444  df-dif 3904  df-in 3908  df-ss 3918  df-nul 4274  df-sn 4578  df-uni 4857

This theorem is referenced by:  csbuni  4888  uniintsn  4939  iununi  5050  unisn2  5260  eqsnuniex  5307  opswap  6171  unixp0  6225  unixpid  6226  unizlim  6427  iotanul  6461  funfv  6915  dffv2  6923  1stval  7905  2ndval  7906  1stnpr  7907  2ndnpr  7908  1st0  7909  2nd0  7910  1st2val  7931  2nd2val  7932  brtpos0  8123  tpostpos  8136  nnunifi  9163  supval2  9316  sup00  9325  infeq5  9498  rankuni  9724  rankxplim3  9742  iunfictbso  9975  cflim2  10124  fin1a2lem11  10271  itunisuc  10280  itunitc  10282  ttukeylem4  10373  relexpfldd  14860  incexclem  15647  arwval  17855  dprdsn  19733  zrhval  20814  0opn  22158  indistopon  22256  mretopd  22348  hauscmplem  22662  cmpfi  22664  comppfsc  22788  alexsublem  23300  alexsubALTlem2  23304  ptcmplem2  23309  lebnumlem3  24231  locfinref  32087  prsiga  32395  sigapildsys  32426  dya2iocuni  32548  fiunelcarsg  32581  carsgclctunlem1  32582  carsgclctunlem3  32585  nnuni  33982  old0  34151  made0  34165  unisnif  34364  limsucncmpi  34771  heicant  35968  ovoliunnfl  35975  voliunnfl  35977  volsupnfl  35978  mbfresfi  35979  stoweidlem35  43964  stoweidlem39  43968  prsal  44247  issalnnd  44272  ismeannd  44394  caragenunicl  44451  isomennd  44458  ipolub0  46696