Theorem inssdif0

Description: Intersection, subclass, and difference relationship. (Contributed by NM, 27-Oct-1996) (Proof shortened by Andrew Salmon, 26-Jun-2011) (Proof shortened by Wolf Lammen, 30-Sep-2014) (Proof shortened by BJ, 18-Jul-2026)

	Ref	Expression
Assertion	inssdif0	$$⊢A\cap B\subseteq C\leftrightarrow A\cap \left(B\setminus C\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		ssdif0	$$⊢A\cap B\subseteq C\leftrightarrow \left(A\cap B\right)\setminus C=\varnothing$$
2		indif2	$$⊢A\cap \left(B\setminus C\right)=\left(A\cap B\right)\setminus C$$
3	2	eqeq1i	$$⊢A\cap \left(B\setminus C\right)=\varnothing \leftrightarrow \left(A\cap B\right)\setminus C=\varnothing$$
4	1 3	bitr4i	$$⊢A\cap B\subseteq C\leftrightarrow A\cap \left(B\setminus C\right)=\varnothing$$