Theorem disjdifb

Description: Relative complement is anticommutative regarding intersection. (Contributed by Zhi Wang, 5-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		indif1	$$⊢\left(A\setminus B\right)\cap \left(B\setminus A\right)=\left(A\cap \left(B\setminus A\right)\right)\setminus B$$
2		disjdif	$$⊢A\cap \left(B\setminus A\right)=\varnothing$$
3	2	difeq1i	$$⊢\left(A\cap \left(B\setminus A\right)\right)\setminus B=\varnothing \setminus B$$
4		0dif	$$⊢\varnothing \setminus B=\varnothing$$
5	1 3 4	3eqtri	$$⊢\left(A\setminus B\right)\cap \left(B\setminus A\right)=\varnothing$$