Theorem uni0 4868

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

Assertion

Ref	Expression
uni0	⊢ ∪ ∅ = ∅

Proof of Theorem uni0

Step	Hyp	Ref	Expression
1		0ss 4352	. 2 ⊢ ∅ ⊆ {∅}
2		uni0b 4866	. 2 ⊢ (∪ ∅ = ∅ ↔ ∅ ⊆ {∅})
3	1, 2	mpbir 233	1 ⊢ ∪ ∅ = ∅

Syntax hints:   = wceq 1537   ⊆ wss 3938  ∅c0 4293  {csn 4569  ∪ cuni 4840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-v 3498  df-dif 3941  df-in 3945  df-ss 3954  df-nul 4294  df-sn 4570  df-uni 4841

This theorem is referenced by:  csbuni  4869  uniintsn  4915  iununi  5023  unisn2  5218  opswap  6088  unixp0  6136  unixpid  6137  unizlim  6309  iotanul  6335  funfv  6752  dffv2  6758  1stval  7693  2ndval  7694  1stnpr  7695  2ndnpr  7696  1st0  7697  2nd0  7698  1st2val  7719  2nd2val  7720  brtpos0  7901  tpostpos  7914  nnunifi  8771  supval2  8921  sup00  8930  infeq5  9102  rankuni  9294  rankxplim3  9312  iunfictbso  9542  cflim2  9687  fin1a2lem11  9834  itunisuc  9843  itunitc  9845  ttukeylem4  9936  incexclem  15193  arwval  17305  dprdsn  19160  zrhval  20657  0opn  21514  indistopon  21611  mretopd  21702  hauscmplem  22016  cmpfi  22018  comppfsc  22142  alexsublem  22654  alexsubALTlem2  22658  ptcmplem2  22663  lebnumlem3  23569  locfinref  31107  prsiga  31392  sigapildsys  31423  dya2iocuni  31543  fiunelcarsg  31576  carsgclctunlem1  31577  carsgclctunlem3  31580  unisnif  33388  limsucncmpi  33795  heicant  34929  ovoliunnfl  34936  voliunnfl  34938  volsupnfl  34939  mbfresfi  34940  stoweidlem35  42327  stoweidlem39  42331  prsal  42610  issalnnd  42635  ismeannd  42756  caragenunicl  42813  isomennd  42820