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 i^i B ) \ B ) = (/) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | inss2 | |- ( A i^i B ) C_ B |
|
| 2 | ssdif0 | |- ( ( A i^i B ) C_ B <-> ( ( A i^i B ) \ B ) = (/) ) |
|
| 3 | 1 2 | mpbi | |- ( ( A i^i B ) \ B ) = (/) |