Description: Equality of restrictions of a function and a subclass. (Contributed by NM, 16-Aug-1994)
Ref | Expression | ||
---|---|---|---|
Assertion | fun2ssres | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resabs1 | |
|
2 | 1 | eqcomd | |
3 | funssres | |
|
4 | 3 | reseq1d | |
5 | 2 4 | sylan9eqr | |
6 | 5 | 3impa | |