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	⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐴 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		funfn	⊢ ( Fun 𝐺 ↔ 𝐺 Fn dom 𝐺 )
2		fvco2	⊢ ( ( 𝐺 Fn dom 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐴 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐴 ) ) )
3	1 2	sylanb	⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐴 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐴 ) ) )