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

Theorem unidm 4114
 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 902 . 2 ((𝑥𝐴𝑥𝐴) ↔ 𝑥𝐴)
21uneqri 4113 1 (𝐴𝐴) = 𝐴
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538   ∈ wcel 2115   ∪ cun 3917 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-un 3924 This theorem is referenced by:  unundi  4132  unundir  4133  uneqin  4240  difabs  4253  undifabs  4409  dfif5  4466  dfsn2  4563  unisng  4843  dfdm2  6119  unixpid  6122  fun2  6531  resasplit  6538  xpider  8364  pm54.43  9427  dmtrclfv  14378  lefld  17836  symg2bas  18521  gsumzaddlem  19041  pwssplit1  19831  plyun0  24797  wlkp1  27474  cycpmco2f1  30798  carsgsigalem  31630  sseqf  31707  probun  31734  nodenselem5  33249  filnetlem3  33785  pibt2  34779  metakunt21  39316  metakunt22  39317  metakunt24  39319  mapfzcons  39573  diophin  39629  pwssplit4  39949  fiuneneq  40057  rclexi  40231  rtrclex  40233  dfrtrcl5  40245  dfrcl2  40291  iunrelexp0  40319  relexpiidm  40321  corclrcl  40324  relexp01min  40330  cotrcltrcl  40342  clsk1indlem3  40665  fiiuncl  41619  fzopredsuc  43806
 Copyright terms: Public domain W3C validator