Theorem unidm 3594

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

Syntax hints:   = wceq 1370   e. wcel 1758   u. cun 3421

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2599  df-v 3067  df-un 3428

This theorem is referenced by:  unundi  3612  unundir  3613  uneqin  3696  difabs  3709  undifabs  3851  dfif5  3900  dfsn2  3985  diftpsn3  4107  unisn  4201  dfdm2  5464  unixpid  5467  fun2  5671  resasplit  5676  xpider  7268  pm54.43  8268  lefld  15495  symg2bas  16002  gsumzaddlem  16509  pwssplit1  17243  plyun0  21778  constr3trllem3  23670  sseqf  26906  probun  26933  filnetlem3  28736  mapfzcons  29187  diophin  29246  pwssplit4  29577  fiuneneq  29697  compne  29831