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

Theorem unidm 3319
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 3318 1  |-  ( A  u.  A )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1685    u. cun 3151
This theorem is referenced by:  unundi  3337  unundir  3338  uneqin  3421  difabs  3433  undifabs  3532  dfif5  3578  dfsn2  3655  unisn  3844  dfdm2  5202  unixpid  5205  fun2  5372  resasplit  5377  xpider  6726  pm54.43  7629  lefld  14344  plyun0  19575  domfldref  24471  inposet  24689  dispos  24698  pgapspf  25463  filnetlem3  25740  mapfzcons  26204  diophin  26263  pwssplit1  26599  pwssplit4  26602  fiuneneq  26924  compne  27053
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 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
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 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-un 3158
  Copyright terms: Public domain W3C validator