This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \subseteq A$

Step	Hyp	Ref	Expression
1		eldifi	$⊢ x \in (A ∖ B) \to x \in A$
2	1	ssriv	$⊢ A ∖ B \subseteq A$