Theorem difin0

Description: The difference of a class from its intersection is empty. Theorem 37 of Suppes p. 29. (Contributed by NM, 17-Aug-2004) (Proof shortened by Andrew Salmon, 26-Jun-2011)

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

Proof

Step	Hyp	Ref	Expression
1		inss2	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
2		ssdif0	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ↔ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐵 ) = ∅ )
3	1 2	mpbi	⊢ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐵 ) = ∅