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

Theorem un0 3480
Description: The union of a class with the empty set is itself. Theorem 24 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
un0  |-  ( A  u.  (/) )  =  A

Proof of Theorem un0
StepHypRef Expression
1 noel 3460 . . . 4  |-  -.  x  e.  (/)
21biorfi 398 . . 3  |-  ( x  e.  A  <->  ( x  e.  A  \/  x  e.  (/) ) )
32bicomi 195 . 2  |-  ( ( x  e.  A  \/  x  e.  (/) )  <->  x  e.  A )
43uneqri 3318 1  |-  ( A  u.  (/) )  =  A
Colors of variables: wff set class
Syntax hints:    \/ wo 359    = wceq 1628    e. wcel 1688    u. cun 3151   (/)c0 3456
This theorem is referenced by:  un00  3491  disjssun  3513  difun2  3534  difdifdir  3542  prprc1  3737  sspr  3778  sstp  3779  iununi  3987  unidif0  4182  suc0  4465  sucprc  4466  fresaun  5377  fresaunres2  5378  fvssunirn  5512  fvun1  5551  fvunsn  5673  fvsnun1  5676  fvsnun2  5677  fsnunfv  5681  fsnunres  5682  fnsuppeq0  5694  funiunfv  5735  difxp1  6115  difxp2  6116  oev2  6517  oarec  6555  undifixp  6847  domss2  7015  domunfican  7124  kmlem2  7772  kmlem3  7773  kmlem11  7781  cda0en  7800  cdaassen  7803  ackbij1lem1  7841  ackbij1lem13  7853  fin1a2lem10  8030  fin1a2lem12  8032  axdc3lem4  8074  ttukeylem6  8136  alephadd  8194  fpwwe2lem13  8259  prunioo  10758  fzsuc2  10836  fseq1p1m1  10851  hashgval  11334  hashinf  11336  hashfun  11383  sadid1  12653  vdwap1  13018  setsres  13168  setsid  13181  mreexexlem3d  13542  mreexdomd  13545  lspsnat  15892  lsppratlem3  15896  opsrtoslem2  16220  indistopon  16732  indistps  16742  indistps2  16743  restcld  16897  filcon  17572  ufildr  17620  ovolioo  18919  itgsplitioo  19186  plyeq0  19587  birthdaylem2  20241  lgsquadlem2  20588  ex-dif  20785  ex-in  20787  ex-res  20803  ballotlemfp1  23043  indispcon  23169  wfrlem14  23670  axfelem9  23755  axfelem10  23756  symdif0  23776  symdifV  23777  symdifid  23778  onint1  24295  sssu  24540  repfuntw  24559  hdrmp  25105  fndifnfp  26155  mapfzcons1  26193  fzsplit1nn0  26232  diophrw  26237  eldioph2lem1  26238  eldioph2lem2  26239  diophren  26295  pwssplit1  26587  pwssplit4  26590  padd01  29267  padd02  29268  pclfinclN  29406
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-dif 3156  df-un 3158  df-nul 3457
  Copyright terms: Public domain W3C validator