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	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 ∖ 𝐵 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		difeq2	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐴 ∖ ∅ ) )
2		difin	⊢ ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 )
3		dif0	⊢ ( 𝐴 ∖ ∅ ) = 𝐴
4	1 2 3	3eqtr3g	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 ∖ 𝐵 ) = 𝐴 )