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

Theorem uni0 4246
Description: The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul 4555 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 3793 . 2  |-  (/)  C_  { (/) }
2 uni0b 4244 . 2  |-  ( U. (/)  =  (/)  <->  (/)  C_  { (/) } )
31, 2mpbir 212 1  |-  U. (/)  =  (/)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    C_ wss 3436   (/)c0 3761   {csn 3998   U.cuni 4219
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-v 3082  df-dif 3439  df-in 3443  df-ss 3450  df-nul 3762  df-sn 3999  df-uni 4220
This theorem is referenced by:  csbuni  4247  uniintsn  4293  iununi  4387  unisn2  4560  opswap  5342  unixp0  5389  unixpid  5390  unizlim  5558  iotanul  5580  funfv  5948  dffv2  5954  1stval  6809  2ndval  6810  1stnpr  6811  2ndnpr  6812  1st0  6813  2nd0  6814  1st2val  6833  2nd2val  6834  brtpos0  6991  tpostpos  7004  nnunifi  7831  supval2  7978  sup00  7987  infeq5  8151  rankuni  8342  rankxplim3  8360  iunfictbso  8552  cflim2  8700  fin1a2lem11  8847  itunisuc  8856  itunitc  8858  ttukeylem4  8949  incexclem  13893  arwval  15937  dprdsn  17668  zrhval  19077  0opn  19932  indistopon  20014  mretopd  20106  hauscmplem  20419  cmpfi  20421  comppfsc  20545  alexsublem  21057  alexsubALTlem2  21061  ptcmplem2  21066  lebnumlem3  21989  lebnumlem3OLD  21992  locfinref  28676  prsiga  28961  sigapildsys  28992  dya2iocuni  29113  fiunelcarsg  29156  carsgclctunlem1  29157  carsgclctunlem3  29160  unisnif  30697  limsucncmpi  31110  heicant  31939  ovoliunnfl  31946  voliunnfl  31948  volsupnfl  31949  mbfresfi  31951  stoweidlem35  37836  stoweidlem39  37840  prsal  38100  ismeannd  38213  caragenunicl  38253  isomennd  38260
  Copyright terms: Public domain W3C validator