Metamath Proof Explorer


Theorem inss1

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

Ref Expression
Assertion inss1 ⊢ A ∩ B ⊆ A

Proof

Step Hyp Ref Expression
1 elinel1 ⊢ x ∈ A ∩ B → x ∈ A
2 1 ssriv ⊢ A ∩ B ⊆ A