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

Metamath Proof Explorer

Theorem ssindif0

Description: Subclass expressed in terms of intersection with difference from the universal class. (Contributed by NM, 17-Sep-2003)

		Ref	Expression
	Assertion	ssindif0	$⊢ A \subseteq B \leftrightarrow A \cap (V ∖ B) = \emptyset$

Step	Hyp	Ref	Expression
1		disj2	$⊢ A \cap (V ∖ B) = \emptyset \leftrightarrow A \subseteq V ∖ (V ∖ B)$
2		ddif	$⊢ V ∖ (V ∖ B) = B$
3	2	sseq2i	$⊢ A \subseteq V ∖ (V ∖ B) \leftrightarrow A \subseteq B$
4	1 3	bitr2i	$⊢ A \subseteq B \leftrightarrow A \cap (V ∖ B) = \emptyset$