Metamath Proof Explorer

Theorem fvco3

Description: Value of a function composition. (Contributed by NM, 3-Jan-2004) (Revised by Mario Carneiro, 26-Dec-2014)

Ref Expression
Assertion fvco3 
|- ( ( G : A --> B /\ C e. A ) -> ( ( F o. G ) ` C ) = ( F ` ( G ` C ) ) )

Proof

Step Hyp Ref Expression
1 ffn 
 |-  ( G : A --> B -> G Fn A )
2 fvco2 
 |-  ( ( G Fn A /\ C e. A ) -> ( ( F o. G ) ` C ) = ( F ` ( G ` C ) ) )
3 1 2 sylan 
 |-  ( ( G : A --> B /\ C e. A ) -> ( ( F o. G ) ` C ) = ( F ` ( G ` C ) ) )