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

Theorem unidm 3717
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 534 . 2 ((𝑥𝐴𝑥𝐴) ↔ 𝑥𝐴)
21uneqri 3716 1 (𝐴𝐴) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wcel 1976  cun 3537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544
This theorem is referenced by:  unundi  3735  unundir  3736  uneqin  3836  difabs  3850  undifabs  3996  dfif5  4051  dfsn2  4137  diftpsn3OLD  4273  unisn  4381  dfdm2  5570  unixpid  5573  fun2  5966  resasplit  5972  xpider  7682  pm54.43  8686  dmtrclfv  13553  lefld  16995  symg2bas  17587  gsumzaddlem  18090  pwssplit1  18826  plyun0  23674  constr3trllem3  25946  carsgsigalem  29510  sseqf  29587  probun  29614  filnetlem3  31351  mapfzcons  36093  diophin  36150  pwssplit4  36473  fiuneneq  36590  rclexi  36737  rtrclex  36739  dfrtrcl5  36751  dfrcl2  36781  iunrelexp0  36809  relexpiidm  36811  corclrcl  36814  relexp01min  36820  cotrcltrcl  36832  clsk1indlem3  37157  compne  37461  fiiuncl  38055  fzopredsuc  39744  1wlkp1  40885
  Copyright terms: Public domain W3C validator