Description: Difference law for subsets. (Contributed by NM, 28-May-1998)
Ref | Expression | ||
---|---|---|---|
Assertion | ssdif | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel | |
|
2 | 1 | anim1d | |
3 | eldif | |
|
4 | eldif | |
|
5 | 2 3 4 | 3imtr4g | |
6 | 5 | ssrdv | |