Theorem unidm 3756

Description: Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
unidm	|- ( A u. A ) = A

Proof of Theorem unidm

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		oridm 536	. 2 |- ( ( x e. A \/ x e. A ) <-> x e. A )
2	1	uneqri 3755	1 |- ( A u. A ) = A

Syntax hints:   = wceq 1483   e. wcel 1990   u. cun 3572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579

This theorem is referenced by:  unundi  3774  unundir  3775  uneqin  3878  difabs  3892  undifabs  4045  dfif5  4102  dfsn2  4190  diftpsn3OLD  4333  unisn  4451  dfdm2  5667  unixpid  5670  fun2  6067  resasplit  6074  xpider  7818  pm54.43  8826  dmtrclfv  13759  lefld  17226  symg2bas  17818  gsumzaddlem  18321  pwssplit1  19059  plyun0  23953  wlkp1  26578  carsgsigalem  30377  sseqf  30454  probun  30481  nodenselem5  31838  filnetlem3  32375  mapfzcons  37279  diophin  37336  pwssplit4  37659  fiuneneq  37775  rclexi  37922  rtrclex  37924  dfrtrcl5  37936  dfrcl2  37966  iunrelexp0  37994  relexpiidm  37996  corclrcl  37999  relexp01min  38005  cotrcltrcl  38017  clsk1indlem3  38341  compneOLD  38644  fiiuncl  39234  fzopredsuc  41333