Theorem unidm 2227

Description: Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27.

Assertion

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

Proof of Theorem unidm

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

Syntax hints:   = wceq 992   e. wcel 994   u. cun 2097

This theorem is referenced by:  unundi 2243  unundir 2244  uneqin 2308  dfsn2 2478  unisn 2583  ac6sfilem3 4590  mapunen 4649  pm54.43 4715  domfldref 10765  fldsqcp2 10780  fldsqcp 10781  scprefat 10783  sqpeq 10786  remcon 10801  inposet 10868  dispos 10881  elfiun 11421  refssfne 11565  hausfillim 11685  fclsfnflim 11726  flimfnfcls 11727

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-un 2102

Copyright terms: Public domain