MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uni0 Structured version   Visualization version   GIF version

Theorem uni0 4831
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 5177. (Revised by Eric Schmidt, 4-Apr-2007.)
Assertion
Ref Expression
uni0 ∅ = ∅

Proof of Theorem uni0
StepHypRef Expression
1 0ss 4307 . 2 ∅ ⊆ {∅}
2 uni0b 4829 . 2 ( ∅ = ∅ ↔ ∅ ⊆ {∅})
31, 2mpbir 234 1 ∅ = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wss 3884  c0 4246  {csn 4528   cuni 4803
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-11 2159  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ral 3114  df-rex 3115  df-v 3446  df-dif 3887  df-in 3891  df-ss 3901  df-nul 4247  df-sn 4529  df-uni 4804
This theorem is referenced by:  csbuni  4832  uniintsn  4878  iununi  4987  unisn2  5183  opswap  6057  unixp0  6106  unixpid  6107  unizlim  6279  iotanul  6306  funfv  6729  dffv2  6737  1stval  7677  2ndval  7678  1stnpr  7679  2ndnpr  7680  1st0  7681  2nd0  7682  1st2val  7703  2nd2val  7704  brtpos0  7886  tpostpos  7899  nnunifi  8757  supval2  8907  sup00  8916  infeq5  9088  rankuni  9280  rankxplim3  9298  iunfictbso  9529  cflim2  9678  fin1a2lem11  9825  itunisuc  9834  itunitc  9836  ttukeylem4  9927  relexpfldd  14405  incexclem  15187  arwval  17299  dprdsn  19155  zrhval  20205  0opn  21513  indistopon  21610  mretopd  21701  hauscmplem  22015  cmpfi  22017  comppfsc  22141  alexsublem  22653  alexsubALTlem2  22657  ptcmplem2  22662  lebnumlem3  23572  locfinref  31198  prsiga  31504  sigapildsys  31535  dya2iocuni  31655  fiunelcarsg  31688  carsgclctunlem1  31689  carsgclctunlem3  31692  unisnif  33500  limsucncmpi  33907  heicant  35091  ovoliunnfl  35098  voliunnfl  35100  volsupnfl  35101  mbfresfi  35102  stoweidlem35  42674  stoweidlem39  42678  prsal  42957  issalnnd  42982  ismeannd  43103  caragenunicl  43160  isomennd  43167
  Copyright terms: Public domain W3C validator