Theorem disjdifb

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

	Ref	Expression
Assertion	disjdifb	|- ( ( A \ B ) i^i ( B \ A ) ) = (/)

Proof

Step	Hyp	Ref	Expression
1		indif1	|- ( ( A \ B ) i^i ( B \ A ) ) = ( ( A i^i ( B \ A ) ) \ B )
2		disjdif	|- ( A i^i ( B \ A ) ) = (/)
3	2	difeq1i	|- ( ( A i^i ( B \ A ) ) \ B ) = ( (/) \ B )
4		0dif	|- ( (/) \ B ) = (/)
5	1 3 4	3eqtri	|- ( ( A \ B ) i^i ( B \ A ) ) = (/)