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

Theorem un0 3810
Description: The union of a class with the empty set is itself. Theorem 24 of [Suppes] p. 27. (Contributed by NM, 15-Jul-1993.)
Assertion
Ref Expression
un0

Proof of Theorem un0
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 noel 3788 . . . 4
21biorfi 407 . . 3
32bicomi 202 . 2
43uneqri 3645 1
Colors of variables: wff setvar class
Syntax hints:  \/wo 368  =wceq 1395  e.wcel 1818  u.cun 3473   c0 3784
This theorem is referenced by:  csbun  3857  un00  3862  disjssun  3884  difun2  3907  difdifdir  3915  disjpr2  4092  prprc1  4140  diftpsn3  4168  sspr  4193  sstp  4194  iununi  4415  unidif0  4625  suc0  4957  sucprc  4958  difxp1  5437  difxp2  5438  fresaun  5761  fresaunres2  5762  fvssunirn  5894  fvun1  5944  fndifnfp  6100  fvunsn  6103  fvsnun1  6106  fvsnun2  6107  fsnunfv  6111  fsnunres  6112  fnsuppeq0OLD  6132  funiunfv  6160  fnsuppeq0  6947  oev2  7192  oarec  7230  undifixp  7525  domss2  7696  domunfican  7813  kmlem2  8552  kmlem3  8553  kmlem11  8561  cda0en  8580  cdaassen  8583  ackbij1lem1  8621  ackbij1lem13  8633  fin1a2lem10  8810  fin1a2lem12  8812  axdc3lem4  8854  ttukeylem6  8915  alephadd  8973  fpwwe2lem13  9041  prunioo  11678  fzsuc2  11766  fseq1p1m1  11781  hashgval  12408  hashinf  12410  hashfun  12495  sadid1  14118  vdwap1  14495  setsres  14660  setsid  14673  mreexexlem3d  15043  mreexdomd  15046  pwssplit1  17705  lspsnat  17791  lsppratlem3  17795  opsrtoslem2  18149  indistopon  19502  indistps  19512  indistps2  19513  restcld  19673  neitr  19681  refun0  20016  filcon  20384  ufildr  20432  restmetu  21090  ovolioo  21978  itgsplitioo  22244  plyeq0  22608  birthdaylem2  23282  lgsquadlem2  23630  constr3pthlem1  24655  ex-dif  25144  ex-in  25146  ex-res  25162  difres  27457  imadifxp  27458  ofpreima2  27508  difico  27594  locfinref  27844  sigaclfu2  28121  prsiga  28131  measun  28182  eulerpartlemt  28310  eulerpartgbij  28311  ballotlemfp1  28430  indispcon  28679  wfrlem14  29356  nofulllem1  29462  nofulllem2  29463  symdif0  29474  symdifV  29475  symdifid  29476  onint1  29914  mapfzcons1  30649  fzsplit1nn0  30687  diophrw  30692  eldioph2lem1  30693  eldioph2lem2  30694  diophren  30747  pwssplit4  31035  dvmptfprodlem  31741  aacllem  33216  bj-pr21val  34571  bj-pr22val  34577  padd01  35535  padd02  35536  pclfinclN  35674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-un 3480  df-nul 3785
  Copyright terms: Public domain W3C validator