Theorem uni0 4835

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

Assertion

Ref	Expression
uni0	⊢ ∪ ∅ = ∅

Proof of Theorem uni0

Step	Hyp	Ref	Expression
1		0ss 4297	. 2 ⊢ ∅ ⊆ {∅}
2		uni0b 4833	. 2 ⊢ (∪ ∅ = ∅ ↔ ∅ ⊆ {∅})
3	1, 2	mpbir 234	1 ⊢ ∪ ∅ = ∅

Syntax hints:   = wceq 1543   ⊆ wss 3853  ∅c0 4223  {csn 4527  ∪ cuni 4805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-11 2160  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-rex 3057  df-v 3400  df-dif 3856  df-in 3860  df-ss 3870  df-nul 4224  df-sn 4528  df-uni 4806

This theorem is referenced by:  csbuni  4836  uniintsn  4884  iununi  4993  unisn2  5190  eqsnuniex  5237  opswap  6072  unixp0  6126  unixpid  6127  unizlim  6308  iotanul  6336  funfv  6776  dffv2  6784  1stval  7741  2ndval  7742  1stnpr  7743  2ndnpr  7744  1st0  7745  2nd0  7746  1st2val  7767  2nd2val  7768  brtpos0  7953  tpostpos  7966  nnunifi  8900  supval2  9049  sup00  9058  infeq5  9230  rankuni  9444  rankxplim3  9462  iunfictbso  9693  cflim2  9842  fin1a2lem11  9989  itunisuc  9998  itunitc  10000  ttukeylem4  10091  relexpfldd  14578  incexclem  15363  arwval  17503  dprdsn  19377  zrhval  20428  0opn  21755  indistopon  21852  mretopd  21943  hauscmplem  22257  cmpfi  22259  comppfsc  22383  alexsublem  22895  alexsubALTlem2  22899  ptcmplem2  22904  lebnumlem3  23814  locfinref  31459  prsiga  31765  sigapildsys  31796  dya2iocuni  31916  fiunelcarsg  31949  carsgclctunlem1  31950  carsgclctunlem3  31953  old0  33729  made0  33743  unisnif  33913  limsucncmpi  34320  heicant  35498  ovoliunnfl  35505  voliunnfl  35507  volsupnfl  35508  mbfresfi  35509  stoweidlem35  43194  stoweidlem39  43198  prsal  43477  issalnnd  43502  ismeannd  43623  caragenunicl  43680  isomennd  43687  ipolub0  45894