Theorem ffund 5335

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

Syntax hints:   -> wi 4   Fun wfun 5176   -->wf 5178

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

This theorem depends on definitions:  df-bi 116  df-fn 5185  df-f 5186

This theorem is referenced by:  ennnfonelemrnh  12286  ennnfonelemf1  12288  ctinfomlemom  12297  cncnp  12771  txcnp  12812  dvidlemap  13201  dvaddxx  13208  dvmulxx  13209  dvcjbr  13213  dvcj  13214  dvrecap  13218