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

Theorem unidm 3450
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 501 . 2  |-  ( ( x  e.  A  \/  x  e.  A )  <->  x  e.  A )
21uneqri 3449 1  |-  ( A  u.  A )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1649    e. wcel 1721    u. cun 3278
This theorem is referenced by:  unundi  3468  unundir  3469  uneqin  3552  difabs  3565  undifabs  3665  dfif5  3711  dfsn2  3788  diftpsn3  3897  unisn  3991  dfdm2  5360  unixpid  5363  fun2  5567  resasplit  5572  xpider  6934  pm54.43  7843  lefld  14626  plyun0  20069  constr3trllem3  21592  probun  24630  filnetlem3  26299  mapfzcons  26662  diophin  26721  pwssplit1  27056  pwssplit4  27059  fiuneneq  27381  compne  27510
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285
  Copyright terms: Public domain W3C validator