Theorem fvcod

Description: Value of a function composition. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	fvcod.g	|- ( ph -> Fun G )
	fvcod.a	|- ( ph -> A e. dom G )
	fvcod.h	|- H = ( F o. G )
Assertion	fvcod	|- ( ph -> ( H ` A ) = ( F ` ( G ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		fvcod.g	|- ( ph -> Fun G )
2		fvcod.a	|- ( ph -> A e. dom G )
3		fvcod.h	|- H = ( F o. G )
4	3	fveq1i	|- ( H ` A ) = ( ( F o. G ) ` A )
5	4	a1i	|- ( ph -> ( H ` A ) = ( ( F o. G ) ` A ) )
6		fvco	|- ( ( Fun G /\ A e. dom G ) -> ( ( F o. G ) ` A ) = ( F ` ( G ` A ) ) )
7	1 2 6	syl2anc	|- ( ph -> ( ( F o. G ) ` A ) = ( F ` ( G ` A ) ) )
8	5 7	eqtrd	|- ( ph -> ( H ` A ) = ( F ` ( G ` A ) ) )