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

Theorem unidm 3320
Description: Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
unidm  |-  ( A  u.  A )  =  A

Proof of Theorem unidm
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 oridm 500 . 2  |-  ( ( x  e.  A  \/  x  e.  A )  <->  x  e.  A )
21uneqri 3319 1  |-  ( A  u.  A )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1625    e. wcel 1686    u. cun 3152
This theorem is referenced by:  unundi  3338  unundir  3339  uneqin  3422  difabs  3434  undifabs  3533  dfif5  3579  dfsn2  3656  unisn  3845  dfdm2  5206  unixpid  5209  fun2  5408  resasplit  5413  xpider  6732  pm54.43  7635  lefld  14350  plyun0  19581  probun  23624  domfldref  25072  inposet  25289  dispos  25298  pgapspf  26063  filnetlem3  26340  mapfzcons  26804  diophin  26863  pwssplit1  27199  pwssplit4  27202  fiuneneq  27524  compne  27653  diftpsneq  28081
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-un 3159
  Copyright terms: Public domain W3C validator