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  7976  2ndval  7977  1stnpr  7978  2ndnpr  7979  1st0  7980  2nd0  7981  1st2val  8002  2nd2val  8003  brtpos0  8217  tpostpos  8230  nnunifi  9293  supval2  9449  sup00  9458  infeq5  9631  rankuni  9857  rankxplim3  9875  iunfictbso  10108  cflim2  10257  fin1a2lem11  10404  itunisuc  10413  itunitc  10415  ttukeylem4  10506  relexpfldd  14996  incexclem  15781  arwval  17992  dprdsn  19905  zrhval  21056  0opn  22405  indistopon  22503  mretopd  22595  hauscmplem  22909  cmpfi  22911  comppfsc  23035  alexsublem  23547  alexsubALTlem2  23551  ptcmplem2  23556  lebnumlem3  24478  old0  27351  made0  27365  locfinref  32816  prsiga  33124  sigapildsys  33155  dya2iocuni  33277  fiunelcarsg  33310  carsgclctunlem1  33311  carsgclctunlem3  33314  nnuni  34691  unisnif  34892  limsucncmpi  35325  heicant  36518  ovoliunnfl  36525  voliunnfl  36527  volsupnfl  36528  mbfresfi  36529  onov0suclim  42014  stoweidlem35  44741  stoweidlem39  44745  prsal  45024  issalnnd  45051  ismeannd  45173  caragenunicl  45230  isomennd  45237  ipolub0  47607