Description: Idempotent law for intersection of classes. Theorem 15 of Suppes p. 26. (Contributed by NM, 5Aug1993)
Ref  Expression  

Assertion  inidm   ( A i^i A ) = A 
Step  Hyp  Ref  Expression 

1  anidm   ( ( x e. A /\ x e. A ) <> x e. A ) 

2  1  ineqri   ( A i^i A ) = A 