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 \left(\mathrm{V}\setminus B\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		disj2	$$⊢A\cap \left(\mathrm{V}\setminus B\right)=\varnothing \leftrightarrow A\subseteq \mathrm{V}\setminus \left(\mathrm{V}\setminus B\right)$$
2		ddif	$$⊢\mathrm{V}\setminus \left(\mathrm{V}\setminus B\right)=B$$
3	2	sseq2i	$$⊢A\subseteq \mathrm{V}\setminus \left(\mathrm{V}\setminus B\right)\leftrightarrow A\subseteq B$$
4	1 3	bitr2i	$$⊢A\subseteq B\leftrightarrow A\cap \left(\mathrm{V}\setminus B\right)=\varnothing$$