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

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

Proof of Theorem uni0
StepHypRef Expression
1 0ss 4347 . 2 ∅ ⊆ {∅}
2 uni0b 4855 . 2 ( ∅ = ∅ ↔ ∅ ⊆ {∅})
31, 2mpbir 232 1 ∅ = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wss 3933  c0 4288  {csn 4557   cuni 4830
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-v 3494  df-dif 3936  df-in 3940  df-ss 3949  df-nul 4289  df-sn 4558  df-uni 4831
This theorem is referenced by:  csbuni  4858  uniintsn  4904  iununi  5012  unisn2  5207  opswap  6079  unixp0  6127  unixpid  6128  unizlim  6300  iotanul  6326  funfv  6743  dffv2  6749  1stval  7680  2ndval  7681  1stnpr  7682  2ndnpr  7683  1st0  7684  2nd0  7685  1st2val  7706  2nd2val  7707  brtpos0  7888  tpostpos  7901  nnunifi  8757  supval2  8907  sup00  8916  infeq5  9088  rankuni  9280  rankxplim3  9298  iunfictbso  9528  cflim2  9673  fin1a2lem11  9820  itunisuc  9829  itunitc  9831  ttukeylem4  9922  incexclem  15179  arwval  17291  dprdsn  19087  zrhval  20583  0opn  21440  indistopon  21537  mretopd  21628  hauscmplem  21942  cmpfi  21944  comppfsc  22068  alexsublem  22580  alexsubALTlem2  22584  ptcmplem2  22589  lebnumlem3  23494  locfinref  31004  prsiga  31289  sigapildsys  31320  dya2iocuni  31440  fiunelcarsg  31473  carsgclctunlem1  31474  carsgclctunlem3  31477  unisnif  33283  limsucncmpi  33690  heicant  34808  ovoliunnfl  34815  voliunnfl  34817  volsupnfl  34818  mbfresfi  34819  stoweidlem35  42197  stoweidlem39  42201  prsal  42480  issalnnd  42505  ismeannd  42626  caragenunicl  42683  isomennd  42690
  Copyright terms: Public domain W3C validator