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 ) C_ A

Proof

Step Hyp Ref Expression
1 eldifi 
 |-  ( x e. ( A \ B ) -> x e. A )
2 1 ssriv 
 |-  ( A \ B ) C_ A