Theorem inidm 2218

Description: Idempotent law for intersection of classes. Theorem 15 of [Suppes] p. 26.

Assertion

Ref	Expression
inidm	|- (A i^i A) = A

Proof of Theorem inidm

Step	Hyp	Ref	Expression
1		anidm 432	. 2 |- ((x e. A /\ x e. A) <-> x e. A)
2	1	ineqri 2205	1 |- (A i^i A) = A

Syntax hints:   = wceq 954   e. wcel 956   i^i cin 2042

This theorem is referenced by:  inindi 2223  inindir 2224  ssin 2228  uneqin 2252  intsn 2559  xpindi 3265  xpindir 3266  rescnvcnv 3485  clmnns 7030  bastgt 7572  indistop 7598  chssoct 9357  chjidmt 9381  mdslmd3 10196  oefil2 10477  filintf 10479

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-in 2047

Copyright terms: Public domain