Description: A class does not intersect a relative complement of a superclass. (Contributed by NM, 24-Mar-1998) Generalize from disjdif . (Revised by BJ, 19-Jul-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | disjdifg | |- ( A C_ B -> ( A i^i ( C \ B ) ) = (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssinss1 | |- ( A C_ B -> ( A i^i C ) C_ B ) |
|
| 2 | inssdif0 | |- ( ( A i^i C ) C_ B <-> ( A i^i ( C \ B ) ) = (/) ) |
|
| 3 | 1 2 | sylib | |- ( A C_ B -> ( A i^i ( C \ B ) ) = (/) ) |