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 \land C \in A) \to (F \circ G) (C) = F (G (C))$

Step	Hyp	Ref	Expression
1		ffn	$⊢ G : A ⟶ B \to G Fn A$
2		fvco2	$⊢ (G Fn A \land C \in A) \to (F \circ G) (C) = F (G (C))$
3	1 2	sylan	$⊢ (G : A ⟶ B \land C \in A) \to (F \circ G) (C) = F (G (C))$