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

Theorem un0 3492
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
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 noel 3472 . . . 4  |-  -.  x  e.  (/)
21biorfi 396 . . 3  |-  ( x  e.  A  <->  ( x  e.  A  \/  x  e.  (/) ) )
32bicomi 193 . 2  |-  ( ( x  e.  A  \/  x  e.  (/) )  <->  x  e.  A )
43uneqri 3330 1  |-  ( A  u.  (/) )  =  A
Colors of variables: wff set class
Syntax hints:    \/ wo 357    = wceq 1632    e. wcel 1696    u. cun 3163   (/)c0 3468
This theorem is referenced by:  un00  3503  disjssun  3525  difun2  3546  difdifdir  3554  prprc1  3749  diftpsn3  3772  sspr  3793  sstp  3794  iununi  4002  unidif0  4199  suc0  4482  sucprc  4483  fresaun  5428  fresaunres2  5429  fvssunirn  5567  fvun1  5606  fvunsn  5728  fvsnun1  5731  fvsnun2  5732  fsnunfv  5736  fsnunres  5737  fnsuppeq0  5749  funiunfv  5790  difxp1  6170  difxp2  6171  oev2  6538  oarec  6576  undifixp  6868  domss2  7036  domunfican  7145  kmlem2  7793  kmlem3  7794  kmlem11  7802  cda0en  7821  cdaassen  7824  ackbij1lem1  7862  ackbij1lem13  7874  fin1a2lem10  8051  fin1a2lem12  8053  axdc3lem4  8095  ttukeylem6  8157  alephadd  8215  fpwwe2lem13  8280  prunioo  10780  fzsuc2  10858  fseq1p1m1  10873  hashgval  11356  hashinf  11358  hashfun  11405  sadid1  12675  vdwap1  13040  setsres  13190  setsid  13203  mreexexlem3d  13564  mreexdomd  13567  lspsnat  15914  lsppratlem3  15918  opsrtoslem2  16242  indistopon  16754  indistps  16764  indistps2  16765  restcld  16919  filcon  17594  ufildr  17642  ovolioo  18941  itgsplitioo  19208  plyeq0  19609  birthdaylem2  20263  lgsquadlem2  20610  ex-dif  20826  ex-in  20828  ex-res  20844  ballotlemfp1  23066  fmptpr  23229  sigaclfu2  23497  prsiga  23507  measxun  23554  indispcon  23780  wfrlem14  24340  nofulllem1  24427  nofulllem2  24428  symdif0  24439  symdifV  24440  symdifid  24441  onint1  24960  sssu  25244  hdrmp  25809  fndifnfp  26859  mapfzcons1  26897  fzsplit1nn0  26936  diophrw  26941  eldioph2lem1  26942  eldioph2lem2  26943  diophren  26999  pwssplit1  27291  pwssplit4  27294  disjpr2  28185  constr3pthlem1  28401  padd01  30622  padd02  30623  pclfinclN  30761
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-dif 3168  df-un 3170  df-nul 3469
  Copyright terms: Public domain W3C validator