Theorem disj4

Description: Two ways of saying that two classes are disjoint. (Contributed by NM, 21-Mar-2004)

	Ref	Expression
Assertion	disj4	$$⊢A\cap B=\varnothing \leftrightarrow \neg A\setminus B\subset A$$

Proof

Step	Hyp	Ref	Expression
1		disj3	$$⊢A\cap B=\varnothing \leftrightarrow A=A\setminus B$$
2		eqcom	$$⊢A=A\setminus B\leftrightarrow A\setminus B=A$$
3		difss	$$⊢A\setminus B\subseteq A$$
4		dfpss2	$$⊢A\setminus B\subset A\leftrightarrow \left(A\setminus B\subseteq A\wedge \neg A\setminus B=A\right)$$
5	3 4	mpbiran	$$⊢A\setminus B\subset A\leftrightarrow \neg A\setminus B=A$$
6	5	con2bii	$$⊢A\setminus B=A\leftrightarrow \neg A\setminus B\subset A$$
7	1 2 6	3bitri	$$⊢A\cap B=\varnothing \leftrightarrow \neg A\setminus B\subset A$$