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		fnsnfv	|- ( ( G Fn A /\ X e. A ) -> { ( G ` X ) } = ( G " { X } ) )
2	1	imaeq2d	|- ( ( G Fn A /\ X e. A ) -> ( F " { ( G ` X ) } ) = ( F " ( G " { X } ) ) )
3		imaco	|- ( ( F o. G ) " { X } ) = ( F " ( G " { X } ) )
4	2 3	syl6reqr	|- ( ( 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 ) ) )