# Metamath Proof Explorer

## Theorem fvco2

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
`|- ( ( G Fn A /\ X e. A ) -> ( ( F o. G ) ` X ) = ( F ` ( G ` X ) ) )`

### Proof

Step Hyp Ref Expression
1 imaco
` |-  ( ( F o. G ) " { X } ) = ( F " ( G " { X } ) )`
2 fnsnfv
` |-  ( ( G Fn A /\ X e. A ) -> { ( G ` X ) } = ( G " { X } ) )`
3 2 imaeq2d
` |-  ( ( G Fn A /\ X e. A ) -> ( F " { ( G ` X ) } ) = ( F " ( G " { X } ) ) )`
4 1 3 eqtr4id
` |-  ( ( G Fn A /\ X e. A ) -> ( ( F o. G ) " { X } ) = ( F " { ( G ` X ) } ) )`
5 4 eleq2d
` |-  ( ( G Fn A /\ X e. A ) -> ( x e. ( ( F o. G ) " { X } ) <-> x e. ( F " { ( G ` X ) } ) ) )`
6 5 iotabidv
` |-  ( ( G Fn A /\ X e. A ) -> ( iota x x e. ( ( F o. G ) " { X } ) ) = ( iota x x e. ( F " { ( G ` X ) } ) ) )`
7 dffv3
` |-  ( ( F o. G ) ` X ) = ( iota x x e. ( ( F o. G ) " { X } ) )`
8 dffv3
` |-  ( F ` ( G ` X ) ) = ( iota x x e. ( F " { ( G ` X ) } ) )`
9 6 7 8 3eqtr4g
` |-  ( ( G Fn A /\ X e. A ) -> ( ( F o. G ) ` X ) = ( F ` ( G ` X ) ) )`