Theorem ffund 5414

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 5413	. 2 |- ( F : A --> B -> Fun F )
3	1, 2	syl 14	1 |- ( ph -> Fun F )

Syntax hints:   -> wi 4   Fun wfun 5253   -->wf 5255

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 5262  df-f 5263

This theorem is referenced by:  ennnfonelemrnh  12660  ennnfonelemf1  12662  ctinfomlemom  12671  psrbaglesuppg  14306  psrelbasfun  14311  cncnp  14574  txcnp  14615  dvidlemap  15035  dvidrelem  15036  dvidsslem  15037  dvaddxx  15047  dvmulxx  15048  dvcjbr  15052  dvcj  15053  dvrecap  15057  plyaddlem1  15091  plymullem1  15092  plycoeid3  15101