Theorem uni0 4735

Description: The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul 5063 by Eric Schmidt.) (Contributed by NM, 16-Sep-1993.) (Revised by Eric Schmidt, 4-Apr-2007.)

Assertion

Ref	Expression
uni0	⊢ ∪ ∅ = ∅

Proof of Theorem uni0

Step	Hyp	Ref	Expression
1		0ss 4230	. 2 ⊢ ∅ ⊆ {∅}
2		uni0b 4733	. 2 ⊢ (∪ ∅ = ∅ ↔ ∅ ⊆ {∅})
3	1, 2	mpbir 223	1 ⊢ ∪ ∅ = ∅

Syntax hints:   = wceq 1507   ⊆ wss 3823  ∅c0 4172  {csn 4435  ∪ cuni 4708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2744

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ral 3087  df-rex 3088  df-v 3411  df-dif 3826  df-in 3830  df-ss 3837  df-nul 4173  df-sn 4436  df-uni 4709

This theorem is referenced by:  csbuni  4736  uniintsn  4782  iununi  4883  unisn2  5069  opswap  5922  unixp0  5969  unixpid  5970  unizlim  6142  iotanul  6164  funfv  6576  dffv2  6582  1stval  7501  2ndval  7502  1stnpr  7503  2ndnpr  7504  1st0  7505  2nd0  7506  1st2val  7527  2nd2val  7528  brtpos0  7700  tpostpos  7713  nnunifi  8562  supval2  8712  sup00  8721  infeq5  8892  rankuni  9084  rankxplim3  9102  iunfictbso  9332  cflim2  9481  fin1a2lem11  9628  itunisuc  9637  itunitc  9639  ttukeylem4  9730  incexclem  15049  arwval  17173  dprdsn  18920  zrhval  20369  0opn  21228  indistopon  21325  mretopd  21416  hauscmplem  21730  cmpfi  21732  comppfsc  21856  alexsublem  22368  alexsubALTlem2  22372  ptcmplem2  22377  lebnumlem3  23282  locfinref  30778  prsiga  31064  sigapildsys  31095  dya2iocuni  31215  fiunelcarsg  31248  carsgclctunlem1  31249  carsgclctunlem3  31252  unisnif  32936  limsucncmpi  33342  heicant  34397  ovoliunnfl  34404  voliunnfl  34406  volsupnfl  34407  mbfresfi  34408  stoweidlem35  41776  stoweidlem39  41780  prsal  42059  issalnnd  42084  ismeannd  42205  caragenunicl  42262  isomennd  42269