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

Theorem unidm 3293
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
StepHypRef Expression
1 oridm 502 . 2  |-  ( ( x  e.  A  \/  x  e.  A )  <->  x  e.  A )
21uneqri 3292 1  |-  ( A  u.  A )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1619    e. wcel 1621    u. cun 3125
This theorem is referenced by:  unundi  3311  unundir  3312  uneqin  3395  difabs  3407  undifabs  3506  dfif5  3551  dfsn2  3628  unisn  3817  dfdm2  5191  unixpid  5194  fun2  5344  resasplit  5349  xpider  6698  pm54.43  7601  lefld  14311  plyun0  19542  domfldref  24428  inposet  24646  dispos  24655  pgapspf  25420  filnetlem3  25697  mapfzcons  26161  diophin  26220  pwssplit1  26556  pwssplit4  26559  fiuneneq  26881  compne  27011
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 1927  ax-ext 2239
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 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-un 3132
  Copyright terms: Public domain W3C validator