Description: The intersection of two classes is a subset of one of them. Part of Exercise 12 of TakeutiZaring p. 18. (Contributed by NM, 27Apr1994)
Ref  Expression  

Assertion  inss1   ( A i^i B ) C_ A 
Step  Hyp  Ref  Expression 

1  elinel1   ( x e. ( A i^i B ) > x e. A ) 

2  1  ssriv   ( A i^i B ) C_ A 