Theorem inidm 2222

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 2209	1 |- (A i^i A) = A

Syntax hints:   = wceq 956   e. wcel 958   i^i cin 2046

This theorem is referenced by:  inindi 2227  inindir 2228  ssin 2232  uneqin 2256  intsn 2564  xpindi 3270  xpindir 3271  rescnvcnv 3493  clmnns 7084  bastgt 7622  indistop 7648  chssoct 9419  chjidmt 9443  mdslmd3 10259  oefil2 10567  filintf 10569

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-in 2051

Copyright terms: Public domain