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

Theorem uni0 3828
Description: The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul 4123 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 3458 . 2  |-  (/)  C_  { (/) }
2 uni0b 3826 . 2  |-  ( U. (/)  =  (/)  <->  (/)  C_  { (/) } )
31, 2mpbir 202 1  |-  U. (/)  =  (/)
Colors of variables: wff set class
Syntax hints:    = wceq 1619    C_ wss 3127   (/)c0 3430   {csn 3614   U.cuni 3801
This theorem is referenced by:  uniintsn  3873  iununi  3960  unizlim  4481  unisn2  4494  opswap  5146  unixp0  5193  unixpid  5194  fvprc  5455  funfv  5520  dffv2  5526  1stval  6058  2ndval  6059  1st0  6060  2nd0  6061  1st2val  6079  2nd2val  6080  brtpos0  6175  tpostpos  6188  iotanul  6240  nnunifi  7076  infeq5  7306  rankuni  7503  rankxplim3  7519  iunfictbso  7709  cflim2  7857  fin1a2lem11  8004  itunisuc  8013  itunitc  8015  ttukeylem4  8107  arwval  13837  dprdsn  15233  zrhval  16424  0opn  16612  indistopon  16700  mretopd  16791  hauscmplem  17095  cmpfi  17097  alexsublem  17700  alexsubALTlem2  17704  ptcmplem2  17709  lebnumlem3  18423  unisnif  23839  funpartfv  23858  limsucncmpi  24259  empos  24609  comppfsc  25674  stoweidlem35  27119  stoweidlem39  27123
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 2239
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 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rex 2524  df-v 2765  df-dif 3130  df-in 3134  df-ss 3141  df-nul 3431  df-sn 3620  df-uni 3802
  Copyright terms: Public domain W3C validator