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

Theorem un0 3479
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 3459 . . . 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 3317 1  |-  ( A  u.  (/) )  =  A
Colors of variables: wff set class
Syntax hints:    \/ wo 357    = wceq 1623    e. wcel 1684    u. cun 3150   (/)c0 3455
This theorem is referenced by:  un00  3490  disjssun  3512  difun2  3533  difdifdir  3541  prprc1  3736  sspr  3777  sstp  3778  iununi  3986  unidif0  4183  suc0  4466  sucprc  4467  fresaun  5412  fresaunres2  5413  fvssunirn  5551  fvun1  5590  fvunsn  5712  fvsnun1  5715  fvsnun2  5716  fsnunfv  5720  fsnunres  5721  fnsuppeq0  5733  funiunfv  5774  difxp1  6154  difxp2  6155  oev2  6522  oarec  6560  undifixp  6852  domss2  7020  domunfican  7129  kmlem2  7777  kmlem3  7778  kmlem11  7786  cda0en  7805  cdaassen  7808  ackbij1lem1  7846  ackbij1lem13  7858  fin1a2lem10  8035  fin1a2lem12  8037  axdc3lem4  8079  ttukeylem6  8141  alephadd  8199  fpwwe2lem13  8264  prunioo  10764  fzsuc2  10842  fseq1p1m1  10857  hashgval  11340  hashinf  11342  hashfun  11389  sadid1  12659  vdwap1  13024  setsres  13174  setsid  13187  mreexexlem3d  13548  mreexdomd  13551  lspsnat  15898  lsppratlem3  15902  opsrtoslem2  16226  indistopon  16738  indistps  16748  indistps2  16749  restcld  16903  filcon  17578  ufildr  17626  ovolioo  18925  itgsplitioo  19192  plyeq0  19593  birthdaylem2  20247  lgsquadlem2  20594  ex-dif  20810  ex-in  20812  ex-res  20828  ballotlemfp1  23050  fmptpr  23214  sigaclfu2  23482  prsiga  23492  measxun  23539  indispcon  23765  wfrlem14  24269  nofulllem1  24356  nofulllem2  24357  symdif0  24368  symdifV  24369  symdifid  24370  onint1  24888  sssu  25141  hdrmp  25706  fndifnfp  26756  mapfzcons1  26794  fzsplit1nn0  26833  diophrw  26838  eldioph2lem1  26839  eldioph2lem2  26840  diophren  26896  pwssplit1  27188  pwssplit4  27191  difprsneq  28068  difprsng  28069  diftpsneq  28070  padd01  30000  padd02  30001  pclfinclN  30139
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155  df-un 3157  df-nul 3456
  Copyright terms: Public domain W3C validator