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	$$⊢\phi \to F:C⟶D$$
	cofmpt.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$
Assertion	cofmpt	$$⊢\phi \to F\circ \left(x\in A⟼B\right)=\left(x\in A⟼F\left(B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cofmpt.1	$$⊢\phi \to F:C⟶D$$
2		cofmpt.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$
3		eqidd	$$⊢\phi \to \left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
4	1	feqmptd	$$⊢\phi \to F=\left(y\in C⟼F\left(y\right)\right)$$
5		fveq2	$$⊢y=B\to F\left(y\right)=F\left(B\right)$$
6	2 3 4 5	fmptco	$$⊢\phi \to F\circ \left(x\in A⟼B\right)=\left(x\in A⟼F\left(B\right)\right)$$