Description: Value of a function composition. Similar to second part of Theorem 3H of Enderton p. 47. (Contributed by NM, 9-Oct-2004) (Proof shortened by Andrew Salmon, 22-Oct-2011) (Revised by Stefan O'Rear, 16-Oct-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | fvco2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imaco | |
|
2 | fnsnfv | |
|
3 | 2 | imaeq2d | |
4 | 1 3 | eqtr4id | |
5 | 4 | eleq2d | |
6 | 5 | iotabidv | |
7 | dffv3 | |
|
8 | dffv3 | |
|
9 | 6 7 8 | 3eqtr4g | |