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  cntzmhm2  14168  psrbaglesuppg  15141  psrelbasfun  15153  cncnp  15422  txcnp  15463  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dvaddxx  15895  dvmulxx  15896  dvcjbr  15900  dvcj  15901  dvrecap  15905  plyaddlem1  15939  plymullem1  15940  plycoeid3  15949  uhgrfun  16484  vdegp1aid  16721  vdegp1bid  16722  wlkres  16786