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

Theorem unidm 3748
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 536 . 2 ((𝑥𝐴𝑥𝐴) ↔ 𝑥𝐴)
21uneqri 3747 1 (𝐴𝐴) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1481  wcel 1988  cun 3565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-un 3572
This theorem is referenced by:  unundi  3766  unundir  3767  uneqin  3870  difabs  3884  undifabs  4036  dfif5  4093  dfsn2  4181  diftpsn3OLD  4324  unisn  4442  dfdm2  5655  unixpid  5658  fun2  6054  resasplit  6061  xpider  7803  pm54.43  8811  dmtrclfv  13740  lefld  17207  symg2bas  17799  gsumzaddlem  18302  pwssplit1  19040  plyun0  23934  wlkp1  26559  carsgsigalem  30351  sseqf  30428  probun  30455  nodenselem5  31812  filnetlem3  32350  mapfzcons  37098  diophin  37155  pwssplit4  37478  fiuneneq  37594  rclexi  37741  rtrclex  37743  dfrtrcl5  37755  dfrcl2  37785  iunrelexp0  37813  relexpiidm  37815  corclrcl  37818  relexp01min  37824  cotrcltrcl  37836  clsk1indlem3  38161  compneOLD  38464  fiiuncl  39054  fzopredsuc  41096
  Copyright terms: Public domain W3C validator