Metamath Proof Explorer

Theorem fvco3

Description: Value of a function composition. (Contributed by NM, 3-Jan-2004) (Revised by Mario Carneiro, 26-Dec-2014)

Ref Expression
Assertion fvco3 ⊢ G : A ⟶ B ∧ C ∈ A → F ∘ G ⁡ C = F ⁡ G ⁡ C

Proof

Step Hyp Ref Expression
1 ffn ⊢ G : A ⟶ B → G Fn A
2 fvco2 ⊢ G Fn A ∧ C ∈ A → F ∘ G ⁡ C = F ⁡ G ⁡ C
3 1 2 sylan ⊢ G : A ⟶ B ∧ C ∈ A → F ∘ G ⁡ C = F ⁡ G ⁡ C