Theorem ffund 5408

Description: A mapping is a function, deduction version. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

Hypothesis

Ref	Expression
ffund.1	|- ( ph -> F : A --> B )

Assertion

Ref	Expression
ffund	|- ( ph -> Fun F )

Proof of Theorem ffund

Step	Hyp	Ref	Expression
1		ffund.1	. 2 |- ( ph -> F : A --> B )
2		ffun 5407	. 2 |- ( F : A --> B -> Fun F )
3	1, 2	syl 14	1 |- ( ph -> Fun F )

Syntax hints:   -> wi 4   Fun wfun 5249   -->wf 5251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-fn 5258  df-f 5259

This theorem is referenced by:  ennnfonelemrnh  12576  ennnfonelemf1  12578  ctinfomlemom  12587  psrbaglesuppg  14169  psrelbasfun  14172  cncnp  14409  txcnp  14450  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dvaddxx  14882  dvmulxx  14883  dvcjbr  14887  dvcj  14888  dvrecap  14892  plyaddlem1  14926  plymullem1  14927