Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif . (Contributed by David Moews, 1-May-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | eldifd.1 | |
|
eldifd.2 | |
||
Assertion | eldifd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldifd.1 | |
|
2 | eldifd.2 | |
|
3 | eldif | |
|
4 | 1 2 3 | sylanbrc | |