Theorem ffund 5512

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

Syntax hints:   -> wi 4   Fun wfun 5346   -->wf 5348

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 5355  df-f 5356

This theorem is referenced by:  swrdwrdsymbg  11356  ennnfonelemrnh  13167  ennnfonelemf1  13169  ctinfomlemom  13178  psrbaglesuppg  14821  psrelbasfun  14832  cncnp  15095  txcnp  15136  dvidlemap  15556  dvidrelem  15557  dvidsslem  15558  dvaddxx  15568  dvmulxx  15569  dvcjbr  15573  dvcj  15574  dvrecap  15578  plyaddlem1  15612  plymullem1  15613  plycoeid3  15622  uhgrfun  16072  vdegp1aid  16309  vdegp1bid  16310  wlkres  16374