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

Theorem unidm 3887
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 537 . 2 ((𝑥𝐴𝑥𝐴) ↔ 𝑥𝐴)
21uneqri 3886 1 (𝐴𝐴) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1620  wcel 2127  cun 3701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-v 3330  df-un 3708
This theorem is referenced by:  unundi  3905  unundir  3906  uneqin  4009  difabs  4023  undifabs  4177  dfif5  4234  dfsn2  4322  diftpsn3OLD  4466  unisn  4591  dfdm2  5816  unixpid  5819  fun2  6216  resasplit  6223  xpider  7973  pm54.43  8987  dmtrclfv  13929  lefld  17398  symg2bas  17989  gsumzaddlem  18492  pwssplit1  19232  plyun0  24123  wlkp1  26759  carsgsigalem  30657  sseqf  30734  probun  30761  nodenselem5  32115  filnetlem3  32652  mapfzcons  37750  diophin  37807  pwssplit4  38130  fiuneneq  38246  rclexi  38393  rtrclex  38395  dfrtrcl5  38407  dfrcl2  38437  iunrelexp0  38465  relexpiidm  38467  corclrcl  38470  relexp01min  38476  cotrcltrcl  38488  clsk1indlem3  38812  compneOLD  39115  fiiuncl  39702  fzopredsuc  41812
  Copyright terms: Public domain W3C validator