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

Theorem uni0 3856
Description: The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul 4151 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 3485 . 2  |-  (/)  C_  { (/) }
2 uni0b 3854 . 2  |-  ( U. (/)  =  (/)  <->  (/)  C_  { (/) } )
31, 2mpbir 202 1  |-  U. (/)  =  (/)
Colors of variables: wff set class
Syntax hints:    = wceq 1624    C_ wss 3154   (/)c0 3457   {csn 3642   U.cuni 3829
This theorem is referenced by:  uniintsn  3901  iununi  3988  unizlim  4509  unisn2  4522  opswap  5158  unixp0  5205  unixpid  5206  fvprc  5483  funfv  5548  dffv2  5554  1stval  6086  2ndval  6087  1st0  6088  2nd0  6089  1st2val  6107  2nd2val  6108  brtpos0  6203  tpostpos  6216  iotanul  6268  nnunifi  7104  infeq5  7334  rankuni  7531  rankxplim3  7547  iunfictbso  7737  cflim2  7885  fin1a2lem11  8032  itunisuc  8041  itunitc  8043  ttukeylem4  8135  incexclem  12290  arwval  13870  dprdsn  15266  zrhval  16457  0opn  16645  indistopon  16733  mretopd  16824  hauscmplem  17128  cmpfi  17130  alexsublem  17733  alexsubALTlem2  17737  ptcmplem2  17742  lebnumlem3  18456  unisnif  23872  funpartfv  23891  limsucncmpi  24292  empos  24642  comppfsc  25707  stoweidlem35  27184  stoweidlem39  27188
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-v 2792  df-dif 3157  df-in 3161  df-ss 3168  df-nul 3458  df-sn 3648  df-uni 3830
  Copyright terms: Public domain W3C validator