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

Theorem unidm 3492
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 502 . 2  |-  ( ( x  e.  A  \/  x  e.  A )  <->  x  e.  A )
21uneqri 3491 1  |-  ( A  u.  A )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1653    e. wcel 1726    u. cun 3320
This theorem is referenced by:  unundi  3510  unundir  3511  uneqin  3594  difabs  3607  undifabs  3707  dfif5  3753  dfsn2  3830  diftpsn3  3939  unisn  4033  dfdm2  5403  unixpid  5406  fun2  5610  resasplit  5615  xpider  6977  pm54.43  7889  lefld  14673  plyun0  20118  constr3trllem3  21641  probun  24679  filnetlem3  26411  mapfzcons  26774  diophin  26833  pwssplit1  27167  pwssplit4  27170  fiuneneq  27492  compne  27621
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-un 3327
  Copyright terms: Public domain W3C validator