Metamath Proof Explorer
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 
$${\u22a2}{A}\cap {B}\subseteq {A}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

elinel1 
$${\u22a2}{x}\in \left({A}\cap {B}\right)\to {x}\in {A}$$ 
2 
1

ssriv 
$${\u22a2}{A}\cap {B}\subseteq {A}$$ 