Description: A subset of a difference does not intersect the subtrahend. (Contributed by Jeff Hankins, 1-Sep-2013) (Proof shortened by Mario Carneiro, 24-Aug-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ssdifin0 | |- ( A C_ ( B \ C ) -> ( A i^i C ) = (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssrin | |- ( A C_ ( B \ C ) -> ( A i^i C ) C_ ( ( B \ C ) i^i C ) ) |
|
| 2 | incom | |- ( ( B \ C ) i^i C ) = ( C i^i ( B \ C ) ) |
|
| 3 | disjdif | |- ( C i^i ( B \ C ) ) = (/) |
|
| 4 | 2 3 | eqtri | |- ( ( B \ C ) i^i C ) = (/) |
| 5 | sseq0 | |- ( ( ( A i^i C ) C_ ( ( B \ C ) i^i C ) /\ ( ( B \ C ) i^i C ) = (/) ) -> ( A i^i C ) = (/) ) |
|
| 6 | 1 4 5 | sylancl | |- ( A C_ ( B \ C ) -> ( A i^i C ) = (/) ) |