Theorem uni0 4935

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 4400	. 2 ⊢ ∅ ⊆ {∅}
2		uni0b 4933	. 2 ⊢ (∪ ∅ = ∅ ↔ ∅ ⊆ {∅})
3	1, 2	mpbir 231	1 ⊢ ∪ ∅ = ∅

Syntax hints:   = wceq 1540   ⊆ wss 3951  ∅c0 4333  {csn 4626  ∪ cuni 4907

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 2007  ax-8 2110  ax-9 2118  ax-11 2157  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-v 3482  df-dif 3954  df-ss 3968  df-nul 4334  df-sn 4627  df-uni 4908

This theorem is referenced by:  csbuni  4936  uniintsn  4985  iununi  5099  unisn2  5312  eqsnuniex  5361  opswap  6249  unixp0  6303  unixpid  6304  unizlim  6507  iotanul  6539  funfv  6996  dffv2  7004  1stval  8016  2ndval  8017  1stnpr  8018  2ndnpr  8019  1st0  8020  2nd0  8021  1st2val  8042  2nd2val  8043  brtpos0  8258  tpostpos  8271  nnunifi  9327  supval2  9495  sup00  9504  infeq5  9677  rankuni  9903  rankxplim3  9921  iunfictbso  10154  cflim2  10303  fin1a2lem11  10450  itunisuc  10459  itunitc  10461  ttukeylem4  10552  relexpfldd  15089  incexclem  15872  arwval  18088  dprdsn  20056  zrhval  21518  0opn  22910  indistopon  23008  mretopd  23100  hauscmplem  23414  cmpfi  23416  comppfsc  23540  alexsublem  24052  alexsubALTlem2  24056  ptcmplem2  24061  lebnumlem3  24995  old0  27898  made0  27912  locfinref  33840  prsiga  34132  sigapildsys  34163  dya2iocuni  34285  fiunelcarsg  34318  carsgclctunlem1  34319  carsgclctunlem3  34322  wevgblacfn  35114  nnuni  35727  unisnif  35926  limsucncmpi  36446  heicant  37662  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  mbfresfi  37673  onov0suclim  43287  stoweidlem35  46050  stoweidlem39  46054  prsal  46333  issalnnd  46360  ismeannd  46482  caragenunicl  46539  isomennd  46546  dftpos5  48774  ipolub0  48881