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

Theorem uni0 4034
Description: The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul 4330 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 3648 . 2  |-  (/)  C_  { (/) }
2 uni0b 4032 . 2  |-  ( U. (/)  =  (/)  <->  (/)  C_  { (/) } )
31, 2mpbir 201 1  |-  U. (/)  =  (/)
Colors of variables: wff set class
Syntax hints:    = wceq 1652    C_ wss 3312   (/)c0 3620   {csn 3806   U.cuni 4007
This theorem is referenced by:  uniintsn  4079  iununi  4167  unizlim  4689  unisn2  4702  opswap  5347  unixp0  5394  unixpid  5395  iotanul  5424  funfv  5781  dffv2  5787  1stval  6342  2ndval  6343  1st0  6344  2nd0  6345  1st2val  6363  2nd2val  6364  brtpos0  6477  tpostpos  6490  nnunifi  7349  infeq5  7581  rankuni  7778  rankxplim3  7794  iunfictbso  7984  cflim2  8132  fin1a2lem11  8279  itunisuc  8288  itunitc  8290  ttukeylem4  8381  incexclem  12604  arwval  14186  dprdsn  15582  zrhval  16777  0opn  16965  indistopon  17053  mretopd  17144  hauscmplem  17457  cmpfi  17459  alexsublem  18063  alexsubALTlem2  18067  ptcmplem2  18072  lebnumlem3  18976  1stnpr  24081  2ndnpr  24082  prsiga  24502  dya2iocuni  24621  unisnif  25720  limsucncmpi  26143  ovoliunnfl  26194  voliunnfl  26196  volsupnfl  26197  mbfresfi  26199  comppfsc  26324  stoweidlem35  27698  stoweidlem39  27702
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-v 2950  df-dif 3315  df-in 3319  df-ss 3326  df-nul 3621  df-sn 3812  df-uni 4008
  Copyright terms: Public domain W3C validator