Theorem disjdifb

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

	Ref	Expression
Assertion	disjdifb	⊢ ( ( 𝐴 ∖ 𝐵 ) ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅

Proof

Step	Hyp	Ref	Expression
1		indif1	⊢ ( ( 𝐴 ∖ 𝐵 ) ∩ ( 𝐵 ∖ 𝐴 ) ) = ( ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) ∖ 𝐵 )
2		disjdif	⊢ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅
3	2	difeq1i	⊢ ( ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) ∖ 𝐵 ) = ( ∅ ∖ 𝐵 )
4		0dif	⊢ ( ∅ ∖ 𝐵 ) = ∅
5	1 3 4	3eqtri	⊢ ( ( 𝐴 ∖ 𝐵 ) ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅