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

Theorem un0 3421
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 3401 . . . 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 3259 1  |-  ( A  u.  (/) )  =  A
Colors of variables: wff set class
Syntax hints:    \/ wo 359    = wceq 1619    e. wcel 1621    u. cun 3092   (/)c0 3397
This theorem is referenced by:  un00  3432  disjssun  3454  difun2  3475  difdifdir  3483  prprc1  3677  sspr  3718  sstp  3719  iununi  3927  unidif0  4121  suc0  4403  sucprc  4404  fresaun  5315  fresaunres2  5316  fvssunirn  5450  fvun1  5489  fvunsn  5611  fvsnun1  5614  fvsnun2  5615  fsnunfv  5619  fsnunres  5620  fnsuppeq0  5632  funiunfv  5673  difxp1  6053  difxp2  6054  oev2  6455  oarec  6493  undifixp  6785  domss2  6953  domunfican  7062  kmlem2  7710  kmlem3  7711  kmlem11  7719  cda0en  7738  cdaassen  7741  ackbij1lem1  7779  ackbij1lem13  7791  fin1a2lem10  7968  fin1a2lem12  7970  axdc3lem4  8012  ttukeylem6  8074  alephadd  8132  fpwwe2lem13  8197  prunioo  10695  fzsuc2  10773  fseq1p1m1  10788  hashgval  11271  hashinf  11273  hashfun  11319  sadid1  12586  vdwap1  12951  setsres  13101  setsid  13114  mreexexlem3d  13475  mreexdomd  13478  lspsnat  15825  lsppratlem3  15829  opsrtoslem2  16153  indistopon  16665  indistps  16675  indistps2  16676  restcld  16830  filcon  17505  ufildr  17553  ovolioo  18852  itgsplitioo  19119  plyeq0  19520  birthdaylem2  20174  lgsquadlem2  20521  ex-dif  20718  ex-in  20720  ex-res  20736  ballotlemfp1  22976  indispcon  23102  wfrlem14  23603  axfelem9  23688  axfelem10  23689  symdif0  23709  symdifV  23710  symdifid  23711  onint1  24228  sssu  24473  repfuntw  24492  hdrmp  25038  fndifnfp  26088  mapfzcons1  26126  fzsplit1nn0  26165  diophrw  26170  eldioph2lem1  26171  eldioph2lem2  26172  diophren  26228  pwssplit1  26520  pwssplit4  26523  padd01  29130  padd02  29131  pclfinclN  29269
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-v 2742  df-dif 3097  df-un 3099  df-nul 3398
  Copyright terms: Public domain W3C validator