Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif . (Contributed by David Moews, 1-May-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | eldifbd.1 | |- ( ph -> A e. ( B \ C ) ) |
|
| Assertion | eldifbd | |- ( ph -> -. A e. C ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eldifbd.1 | |- ( ph -> A e. ( B \ C ) ) |
|
| 2 | eldif | |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) ) |
|
| 3 | 1 2 | sylib | |- ( ph -> ( A e. B /\ -. A e. C ) ) |
| 4 | 3 | simprd | |- ( ph -> -. A e. C ) |