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

Theorem uni0 3795
Description: The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul 4089 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 3425 . 2  |-  (/)  C_  { (/) }
2 uni0b 3793 . 2  |-  ( U. (/)  =  (/)  <->  (/)  C_  { (/) } )
31, 2mpbir 202 1  |-  U. (/)  =  (/)
Colors of variables: wff set class
Syntax hints:    = wceq 1619    C_ wss 3094   (/)c0 3397   {csn 3581   U.cuni 3768
This theorem is referenced by:  uniintsn  3840  iununi  3927  unizlim  4446  unisn2  4459  opswap  5111  unixp0  5158  unixpid  5159  fvprc  5420  funfv  5485  dffv2  5491  1stval  6023  2ndval  6024  1st0  6025  2nd0  6026  1st2val  6044  2nd2val  6045  brtpos0  6140  tpostpos  6153  iotanul  6205  nnunifi  7041  infeq5  7271  rankuni  7468  rankxplim3  7484  iunfictbso  7674  cflim2  7822  fin1a2lem11  7969  itunisuc  7978  itunitc  7980  ttukeylem4  8072  arwval  13802  dprdsn  15198  zrhval  16389  0opn  16577  indistopon  16665  mretopd  16756  hauscmplem  17060  cmpfi  17062  alexsublem  17665  alexsubALTlem2  17669  ptcmplem2  17674  lebnumlem3  18388  unisnif  23804  funpartfv  23823  limsucncmpi  24224  empos  24574  comppfsc  25639  stoweidlem35  27084  stoweidlem39  27088
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2520  df-rex 2521  df-v 2742  df-dif 3097  df-in 3101  df-ss 3108  df-nul 3398  df-sn 3587  df-uni 3769
  Copyright terms: Public domain W3C validator