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

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

Proof of Theorem uni0
StepHypRef Expression
1 0ss 3483 . 2  |-  (/)  C_  { (/) }
2 uni0b 3852 . 2  |-  ( U. (/)  =  (/)  <->  (/)  C_  { (/) } )
31, 2mpbir 200 1  |-  U. (/)  =  (/)
Colors of variables: wff set class
Syntax hints:    = wceq 1623    C_ wss 3152   (/)c0 3455   {csn 3640   U.cuni 3827
This theorem is referenced by:  uniintsn  3899  iununi  3986  unizlim  4509  unisn2  4522  opswap  5159  unixp0  5206  unixpid  5207  iotanul  5234  funfv  5586  dffv2  5592  1stval  6124  2ndval  6125  1st0  6126  2nd0  6127  1st2val  6145  2nd2val  6146  brtpos0  6241  tpostpos  6254  nnunifi  7108  infeq5  7338  rankuni  7535  rankxplim3  7551  iunfictbso  7741  cflim2  7889  fin1a2lem11  8036  itunisuc  8045  itunitc  8047  ttukeylem4  8139  incexclem  12295  arwval  13875  dprdsn  15271  zrhval  16462  0opn  16650  indistopon  16738  mretopd  16829  hauscmplem  17133  cmpfi  17135  alexsublem  17738  alexsubALTlem2  17742  ptcmplem2  17747  lebnumlem3  18461  1stnpr  23245  2ndnpr  23246  prsiga  23492  unisnif  24464  funpartfv  24483  limsucncmpi  24884  empos  25242  comppfsc  26307  stoweidlem35  27784  stoweidlem39  27788
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-v 2790  df-dif 3155  df-in 3159  df-ss 3166  df-nul 3456  df-sn 3646  df-uni 3828
  Copyright terms: Public domain W3C validator