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

Theorem unidm 3718
 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 3717 1 (𝐴𝐴) = 𝐴
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475   ∈ wcel 1977   ∪ cun 3538 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545 This theorem is referenced by:  unundi  3736  unundir  3737  uneqin  3837  difabs  3851  undifabs  3997  dfif5  4052  dfsn2  4138  diftpsn3OLD  4274  unisn  4387  dfdm2  5584  unixpid  5587  fun2  5980  resasplit  5987  xpider  7705  pm54.43  8709  dmtrclfv  13607  lefld  17049  symg2bas  17641  gsumzaddlem  18144  pwssplit1  18880  plyun0  23757  constr3trllem3  26180  carsgsigalem  29704  sseqf  29781  probun  29808  filnetlem3  31545  mapfzcons  36297  diophin  36354  pwssplit4  36677  fiuneneq  36794  rclexi  36941  rtrclex  36943  dfrtrcl5  36955  dfrcl2  36985  iunrelexp0  37013  relexpiidm  37015  corclrcl  37018  relexp01min  37024  cotrcltrcl  37036  clsk1indlem3  37361  compne  37665  fiiuncl  38259  fzopredsuc  39946  1wlkp1  40890
 Copyright terms: Public domain W3C validator