Description: Value of a function composition. Similar to Exercise 5 of TakeutiZaring p. 28. (Contributed by NM, 22-Apr-2006) (Proof shortened by Mario Carneiro, 26-Dec-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fvco | |- ( ( Fun G /\ A e. dom G ) -> ( ( F o. G ) ` A ) = ( F ` ( G ` A ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | funfn | |- ( Fun G <-> G Fn dom G ) |
|
| 2 | fvco2 | |- ( ( G Fn dom G /\ A e. dom G ) -> ( ( F o. G ) ` A ) = ( F ` ( G ` A ) ) ) |
|
| 3 | 1 2 | sylanb | |- ( ( Fun G /\ A e. dom G ) -> ( ( F o. G ) ` A ) = ( F ` ( G ` A ) ) ) |