Theorem uni0 4902

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

Assertion

Ref	Expression
uni0	⊢ ∪ ∅ = ∅

Proof of Theorem uni0

Step	Hyp	Ref	Expression
1		0ss 4366	. 2 ⊢ ∅ ⊆ {∅}
2		uni0b 4900	. 2 ⊢ (∪ ∅ = ∅ ↔ ∅ ⊆ {∅})
3	1, 2	mpbir 231	1 ⊢ ∪ ∅ = ∅

Syntax hints:   = wceq 1540   ⊆ wss 3917  ∅c0 4299  {csn 4592  ∪ cuni 4874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-v 3452  df-dif 3920  df-ss 3934  df-nul 4300  df-sn 4593  df-uni 4875

This theorem is referenced by:  csbuni  4903  uniintsn  4952  iununi  5066  unisn2  5270  eqsnuniex  5319  opswap  6205  unixp0  6259  unixpid  6260  unizlim  6460  iotanul  6492  funfv  6951  dffv2  6959  1stval  7973  2ndval  7974  1stnpr  7975  2ndnpr  7976  1st0  7977  2nd0  7978  1st2val  7999  2nd2val  8000  brtpos0  8215  tpostpos  8228  nnunifi  9245  supval2  9413  sup00  9423  infeq5  9597  rankuni  9823  rankxplim3  9841  iunfictbso  10074  cflim2  10223  fin1a2lem11  10370  itunisuc  10379  itunitc  10381  ttukeylem4  10472  relexpfldd  15023  incexclem  15809  arwval  18012  dprdsn  19975  zrhval  21424  0opn  22798  indistopon  22895  mretopd  22986  hauscmplem  23300  cmpfi  23302  comppfsc  23426  alexsublem  23938  alexsubALTlem2  23942  ptcmplem2  23947  lebnumlem3  24869  old0  27774  made0  27792  locfinref  33838  prsiga  34128  sigapildsys  34159  dya2iocuni  34281  fiunelcarsg  34314  carsgclctunlem1  34315  carsgclctunlem3  34318  wevgblacfn  35103  nnuni  35721  unisnif  35920  limsucncmpi  36440  heicant  37656  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  mbfresfi  37667  onov0suclim  43270  stoweidlem35  46040  stoweidlem39  46044  prsal  46323  issalnnd  46350  ismeannd  46472  caragenunicl  46529  isomennd  46536  dftpos5  48866  ipolub0  48984