Theorem fvco

Description: Value of a function composition. Similar to Exercise 5 of TakeutiZaring p. 28. (Contributed by NM, 22-Apr-2006) (Proof shortened by Mario Carneiro, 26-Dec-2014)

	Ref	Expression
Assertion	fvco	$$⊢\left(\mathrm{Fun}G\wedge A\in \mathrm{dom}G\right)\to \left(F\circ G\right)\left(A\right)=F\left(G\left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		funfn	$$⊢\mathrm{Fun}G\leftrightarrow GFn\mathrm{dom}G$$
2		fvco2	$$⊢\left(GFn\mathrm{dom}G\wedge A\in \mathrm{dom}G\right)\to \left(F\circ G\right)\left(A\right)=F\left(G\left(A\right)\right)$$
3	1 2	sylanb	$$⊢\left(\mathrm{Fun}G\wedge A\in \mathrm{dom}G\right)\to \left(F\circ G\right)\left(A\right)=F\left(G\left(A\right)\right)$$