Theorem inidm 2225

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 434	. 2 |- ((x e. A /\ x e. A) <-> x e. A)
2	1	ineqri 2212	1 |- (A i^i A) = A

Syntax hints:   = wceq 958   e. wcel 960   i^i cin 2049

This theorem is referenced by:  inindi 2230  inindir 2231  ssin 2235  uneqin 2259  intsn 2568  xpindi 3276  xpindir 3277  rescnvcnv 3499  clmnns 7084  bastgt 7621  indistop 7645  chssoct 9414  chjidmt 9438  mdslmd3 10254  oefil2 10552  filintf 10554

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-in 2054

Copyright terms: Public domain