Metamath Proof Explorer


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 A B B =

Proof

Step Hyp Ref Expression
1 inss2 A B B
2 ssdif0 A B B A B B =
3 1 2 mpbi A B B =