Description: The 2nd (second component of an ordered pair) function restricted to a function F is a function from F into the codomain of F . (Contributed by Alexander van der Vekens, 4-Feb-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | f2ndf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f2ndres | |
|
2 | fssxp | |
|
3 | fssres | |
|
4 | 1 2 3 | sylancr | |
5 | 2 | resabs1d | |
6 | 5 | eqcomd | |
7 | 6 | feq1d | |
8 | 4 7 | mpbird | |