Theorem cofmpt

Description: Express composition of a maps-to function with another function in a maps-to notation. (Contributed by Thierry Arnoux, 29-Jun-2017)

	Ref	Expression
Hypotheses	cofmpt.1	|- ( ph -> F : C --> D )
	cofmpt.2	|- ( ( ph /\ x e. A ) -> B e. C )
Assertion	cofmpt	|- ( ph -> ( F o. ( x e. A |-> B ) ) = ( x e. A |-> ( F ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		cofmpt.1	|- ( ph -> F : C --> D )
2		cofmpt.2	|- ( ( ph /\ x e. A ) -> B e. C )
3		eqidd	|- ( ph -> ( x e. A |-> B ) = ( x e. A |-> B ) )
4	1	feqmptd	|- ( ph -> F = ( y e. C |-> ( F ` y ) ) )
5		fveq2	|- ( y = B -> ( F ` y ) = ( F ` B ) )
6	2 3 4 5	fmptco	|- ( ph -> ( F o. ( x e. A |-> B ) ) = ( x e. A |-> ( F ` B ) ) )