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 
⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 
Proof
Step 
Hyp 
Ref 
Expression 
1 

elinel1 
⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) → 𝑥 ∈ 𝐴 ) 
2 
1

ssriv 
⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 