Theorem ffund 5537

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

This proof depends on syntax axioms:   -> wi 4   Fun wfun 5371   -->wf 5373

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-fn 5380  df-f 5381

This theorem is used by:  swrdwrdsymbg  11452  ennnfonelemrnh  13359  ennnfonelemf1  13361  ctinfomlemom  13370  psrbaglesuppg  15109  psrelbasfun  15121  cncnp  15384  txcnp  15425  dvidlemap  15845  dvidrelem  15846  dvidsslem  15847  dvaddxx  15857  dvmulxx  15858  dvcjbr  15862  dvcj  15863  dvrecap  15867  plyaddlem1  15901  plymullem1  15902  plycoeid3  15911  uhgrfun  16446  vdegp1aid  16683  vdegp1bid  16684  wlkres  16748