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

Theorem un0 3386
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 3366 . . . 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 3227 1  |-  ( A  u.  (/) )  =  A
Colors of variables: wff set class
Syntax hints:    \/ wo 359    = wceq 1619    e. wcel 1621    u. cun 3076   (/)c0 3362
This theorem is referenced by:  un00  3397  disjssun  3419  difun2  3439  difdifdir  3447  prprc1  3640  sspr  3677  sstp  3678  iununi  3884  unidif0  4077  suc0  4359  sucprc  4360  fresaun  5269  fresaunres2  5270  fvssunirn  5404  fvun1  5442  fvunsn  5564  fvsnun1  5567  fvsnun2  5568  fsnunfv  5572  fsnunres  5573  fnsuppeq0  5585  funiunfv  5626  difxp1  6006  difxp2  6007  oev2  6408  oarec  6446  undifixp  6738  domss2  6905  domunfican  7014  kmlem2  7661  kmlem3  7662  kmlem11  7670  cda0en  7689  cdaassen  7692  ackbij1lem1  7730  ackbij1lem13  7742  fin1a2lem10  7919  fin1a2lem12  7921  axdc3lem4  7963  ttukeylem6  8025  alephadd  8079  fpwwe2lem13  8144  prunioo  10642  fzsuc2  10720  fseq1p1m1  10735  hashgval  11218  hashinf  11220  hashfun  11266  sadid1  12533  vdwap1  12898  setsres  13048  setsid  13061  lspsnat  15732  lsppratlem3  15736  opsrtoslem2  16058  indistopon  16570  indistps  16580  indistps2  16581  restcld  16735  filcon  17410  ufildr  17458  ovolioo  18757  itgsplitioo  19024  plyeq0  19425  birthdaylem2  20079  lgsquadlem2  20426  ex-dif  20623  ex-in  20625  ex-res  20641  indispcon  22936  wfrlem14  23437  axfelem9  23522  axfelem10  23523  symdif0  23543  symdifV  23544  symdifid  23545  onint1  24062  sssu  24307  repfuntw  24326  hdrmp  24872  fndifnfp  25922  mapfzcons1  25960  fzsplit1nn0  25999  diophrw  26004  eldioph2lem1  26005  eldioph2lem2  26006  diophren  26062  pwssplit1  26354  pwssplit4  26357  padd01  28689  padd02  28690  pclfinclN  28828
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-dif 3081  df-un 3083  df-nul 3363
  Copyright terms: Public domain W3C validator