Theorem disjdif2

Description: The difference of a class and a class disjoint from it is the original class. (Contributed by BJ, 21-Apr-2019)

	Ref	Expression
Assertion	disjdif2	$$⊢A\cap B=\varnothing \to A\setminus B=A$$

Proof

Step	Hyp	Ref	Expression
1		difeq2	$$⊢A\cap B=\varnothing \to A\setminus \left(A\cap B\right)=A\setminus \varnothing$$
2		difin	$$⊢A\setminus \left(A\cap B\right)=A\setminus B$$
3		dif0	$$⊢A\setminus \varnothing =A$$
4	1 2 3	3eqtr3g	$$⊢A\cap B=\varnothing \to A\setminus B=A$$