Metamath Proof Explorer


Theorem fnfco

Description: Composition of two functions. (Contributed by NM, 22-May-2006)

Ref Expression
Assertion fnfco F Fn A G : B A F G Fn B

Proof

Step Hyp Ref Expression
1 df-f G : B A G Fn B ran G A
2 fnco F Fn A G Fn B ran G A F G Fn B
3 2 3expb F Fn A G Fn B ran G A F G Fn B
4 1 3 sylan2b F Fn A G : B A F G Fn B