Theorem disjdifr

Description: A class and its relative complement are disjoint. (Contributed by Thierry Arnoux, 29-Nov-2023)

	Ref	Expression
Assertion	disjdifr	$$⊢\left(B\setminus A\right)\cap A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		incom	$$⊢A\cap \left(B\setminus A\right)=\left(B\setminus A\right)\cap A$$
2		disjdif	$$⊢A\cap \left(B\setminus A\right)=\varnothing$$
3	1 2	eqtr3i	$$⊢\left(B\setminus A\right)\cap A=\varnothing$$