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

Theorem unidm 4117
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 904 . 2 ((𝑥𝐴𝑥𝐴) ↔ 𝑥𝐴)
21uneqri 4116 1 (𝐴𝐴) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wcel 2107  cun 3913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-un 3920
This theorem is referenced by:  unundi  4135  unundir  4136  uneqin  4243  difabs  4258  undifabs  4442  dfif5  4507  dfsn2  4604  unisng  4891  dfdm2  6238  unixpid  6241  fun2  6710  resasplit  6717  xpider  8734  pm54.43  9944  dmtrclfv  14910  lefld  18488  symg2bas  19181  gsumzaddlem  19705  pwssplit1  20536  plyun0  25574  nodenselem5  27052  addsproplem6  27308  wlkp1  28671  cycpmco2f1  32015  carsgsigalem  32955  sseqf  33032  probun  33059  filnetlem3  34881  pibt2  35917  metakunt21  40626  metakunt22  40627  metakunt24  40629  mapfzcons  41068  diophin  41124  pwssplit4  41445  fiuneneq  41553  rclexi  41961  rtrclex  41963  dfrtrcl5  41975  dfrcl2  42020  iunrelexp0  42048  relexpiidm  42050  corclrcl  42053  relexp01min  42059  cotrcltrcl  42071  clsk1indlem3  42389  fiiuncl  43347  fzopredsuc  45629
  Copyright terms: Public domain W3C validator