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 ABA

Proof

Step Hyp Ref Expression
1 eldifi xABxA
2 1 ssriv ABA