Metamath Proof Explorer


Theorem difss

Description: Subclass relationship for class difference. Exercise 14 of TakeutiZaring p. 22. (Contributed by NM, 29-Apr-1994)

Ref Expression
Assertion difss ⊢ A ∖ B ⊆ A

Proof

Step Hyp Ref Expression
1 eldifi ⊢ x ∈ A ∖ B → x ∈ A
2 1 ssriv ⊢ A ∖ B ⊆ A