Theorem unidm 3633

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 512	. 2 |- ( ( x e. A \/ x e. A ) <-> x e. A )
2	1	uneqri 3632	1 |- ( A u. A ) = A

Syntax hints:   = wceq 1398   e. wcel 1823   u. cun 3459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466

This theorem is referenced by:  unundi  3651  unundir  3652  uneqin  3746  difabs  3759  undifabs  3893  dfif5  3945  dfsn2  4029  diftpsn3  4154  unisn  4250  dfdm2  5522  unixpid  5525  fun2  5731  resasplit  5737  xpider  7374  pm54.43  8372  dmtrclfv  12936  lefld  16055  symg2bas  16622  gsumzaddlem  17133  pwssplit1  17900  plyun0  22760  constr3trllem3  24854  carsgsigalem  28523  sseqf  28595  probun  28622  filnetlem3  30438  mapfzcons  30888  diophin  30945  pwssplit4  31274  fiuneneq  31395  compne  31590  dfrcl2  38193  relexp01min  38219  relexpiidm  38222  iunrelexp0  38224  corclrcl  38230  cotrcltrcl  38233