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

Theorem unidm 3789
Description: Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
unidm (𝐴𝐴) = 𝐴

Proof of Theorem unidm
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 oridm 535 . 2 ((𝑥𝐴𝑥𝐴) ↔ 𝑥𝐴)
21uneqri 3788 1 (𝐴𝐴) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  wcel 2030  cun 3605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612
This theorem is referenced by:  unundi  3807  unundir  3808  uneqin  3911  difabs  3925  undifabs  4078  dfif5  4135  dfsn2  4223  diftpsn3OLD  4365  unisn  4483  dfdm2  5705  unixpid  5708  fun2  6105  resasplit  6112  xpider  7861  pm54.43  8864  dmtrclfv  13803  lefld  17273  symg2bas  17864  gsumzaddlem  18367  pwssplit1  19107  plyun0  23998  wlkp1  26634  carsgsigalem  30505  sseqf  30582  probun  30609  nodenselem5  31963  filnetlem3  32500  mapfzcons  37596  diophin  37653  pwssplit4  37976  fiuneneq  38092  rclexi  38239  rtrclex  38241  dfrtrcl5  38253  dfrcl2  38283  iunrelexp0  38311  relexpiidm  38313  corclrcl  38316  relexp01min  38322  cotrcltrcl  38334  clsk1indlem3  38658  compneOLD  38961  fiiuncl  39548  fzopredsuc  41658
  Copyright terms: Public domain W3C validator