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

Theorem un0 3440
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 3420 . . . 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 3278 1  |-  ( A  u.  (/) )  =  A
Colors of variables: wff set class
Syntax hints:    \/ wo 359    = wceq 1619    e. wcel 1621    u. cun 3111   (/)c0 3416
This theorem is referenced by:  un00  3451  disjssun  3473  difun2  3494  difdifdir  3502  prprc1  3696  sspr  3737  sstp  3738  iununi  3946  unidif0  4141  suc0  4424  sucprc  4425  fresaun  5336  fresaunres2  5337  fvssunirn  5471  fvun1  5510  fvunsn  5632  fvsnun1  5635  fvsnun2  5636  fsnunfv  5640  fsnunres  5641  fnsuppeq0  5653  funiunfv  5694  difxp1  6074  difxp2  6075  oev2  6476  oarec  6514  undifixp  6806  domss2  6974  domunfican  7083  kmlem2  7731  kmlem3  7732  kmlem11  7740  cda0en  7759  cdaassen  7762  ackbij1lem1  7800  ackbij1lem13  7812  fin1a2lem10  7989  fin1a2lem12  7991  axdc3lem4  8033  ttukeylem6  8095  alephadd  8153  fpwwe2lem13  8218  prunioo  10716  fzsuc2  10794  fseq1p1m1  10809  hashgval  11292  hashinf  11294  hashfun  11340  sadid1  12607  vdwap1  12972  setsres  13122  setsid  13135  mreexexlem3d  13496  mreexdomd  13499  lspsnat  15846  lsppratlem3  15850  opsrtoslem2  16174  indistopon  16686  indistps  16696  indistps2  16697  restcld  16851  filcon  17526  ufildr  17574  ovolioo  18873  itgsplitioo  19140  plyeq0  19541  birthdaylem2  20195  lgsquadlem2  20542  ex-dif  20739  ex-in  20741  ex-res  20757  ballotlemfp1  22997  indispcon  23123  wfrlem14  23624  axfelem9  23709  axfelem10  23710  symdif0  23730  symdifV  23731  symdifid  23732  onint1  24249  sssu  24494  repfuntw  24513  hdrmp  25059  fndifnfp  26109  mapfzcons1  26147  fzsplit1nn0  26186  diophrw  26191  eldioph2lem1  26192  eldioph2lem2  26193  diophren  26249  pwssplit1  26541  pwssplit4  26544  padd01  29151  padd02  29152  pclfinclN  29290
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 2759  df-dif 3116  df-un 3118  df-nul 3417
  Copyright terms: Public domain W3C validator