Theorem ffund 6613

Description: A mapping is a function, deduction version. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

Hypothesis

Ref	Expression
ffund.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

Ref	Expression
ffund	⊢ (𝜑 → Fun 𝐹)

Proof of Theorem ffund

Step	Hyp	Ref	Expression
1		ffund.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		ffun 6612	. 2 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)
3	1, 2	syl 17	1 ⊢ (𝜑 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 6431  ⟶wf 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 397  df-fn 6440  df-f 6441

This theorem is referenced by:  fofun  6698  fmptco  7010  funfvima2d  7117  smores2  8194  elmapfun  8663  fdmfifsupp  9147  fsuppmptif  9167  fsuppco2  9171  fsuppcor  9172  ordtypelem8  9293  ordtypelem9  9294  ordtypelem10  9295  unxpwdom2  9356  fpwwe2  10408  swrdwrdsymb  14384  mrcuni  17339  frmdss2  18511  cntzmhm2  18955  frgpupval  19389  gsumzadd  19532  gsumpt  19572  gsum2dlem2  19581  dprd2da  19654  lmhmpreima  20319  lmhmlsp  20320  cygznlem2  20785  frlmsslsp  21012  frlmup1  21014  frlmup4  21017  lindff1  21036  lindfrn  21037  psrelbasfun  21158  mvrcl  21230  evlslem3  21299  evlseu  21302  mpfind  21326  mhpmulcl  21348  gsumply1subr  21414  cnclsi  22432  cncnp  22440  paste  22454  connima  22585  1stcfb  22605  1stccnp  22622  1stckgenlem  22713  txcnpi  22768  txcnp  22780  xkoco2cn  22818  fmfnfmlem2  23115  lmflf  23165  txflf  23166  cnextcn  23227  clssubg  23269  ghmcnp  23275  metustid  23719  metustexhalf  23721  isngp2  23762  pi1xfrval  24226  pi1coval  24232  iscfil2  24439  rrxcph  24565  ismbfd  24812  ellimc2  25050  ellimc3  25052  dvres3  25086  dvres3a  25087  dvcnv  25150  dvcnvrelem1  25190  ftc1cn  25216  mdegldg  25240  plyeq0  25381  plyaddlem1  25383  plymullem1  25384  ulmdv  25571  dchrelbas2  26394  dchrghm  26413  uhgrfun  27445  vdegp1ai  27912  vdegp1bi  27913  wlkres  28047  sspg  29099  ssps  29101  sspn  29107  htthlem  29288  fmptcof2  31003  fnpreimac  31017  curry2ima  31050  offinsupp1  31071  fpwrelmapffslem  31076  swrdrn2  31235  pwrssmgc  31287  gsumhashmul  31325  xrge0tsmsd  31326  cyc3co2  31416  tocyccntz  31420  rmfsupp2  31501  rhmpreimaidl  31612  elrspunidl  31615  rhmimaidl  31618  lbsdiflsp0  31716  fedgmullem1  31719  fedgmullem2  31720  rhmpreimacnlem  31843  esumpfinvallem  32051  sibfof  32316  sitgclg  32318  eulerpartlemd  32342  eulerpartlemgu  32353  eulerpartlemgf  32355  dstrvprob  32447  dstfrvel  32449  orvclteinc  32451  spthcycl  33100  cvmliftmolem1  33252  cvmliftlem3  33258  cvmliftlem10  33265  cvmliftlem13  33267  cvmlift2lem9  33282  cvmlift3lem6  33295  cvmlift3lem7  33296  satefvfmla0  33389  satefvfmla1  33396  msubrn  33500  mclsax  33540  mclsppslem  33554  mclspps  33555  ftc1cnnc  35858  heibor1lem  35976  grpokerinj  36060  sticksstones1  40109  lmhmfgima  40916  gneispacefun  41754  cncmpmax  42582  fidmfisupp  42746  limccog  43168  limsuppnfdlem  43249  climxrrelem  43297  climxrre  43298  liminfvalxr  43331  liminflimsupxrre  43365  xlimxrre  43379  dvsinax  43461  fvvolioof  43537  fvvolicof  43539  dirkercncflem2  43652  fourierdlem82  43736  subsaliuncllem  43903  fge0iccico  43915  sge0sn  43924  sge0tsms  43925  sge0cl  43926  sge0f1o  43927  sge0isum  43972  ovnovollem1  44201  ovnovollem2  44202  preimaioomnf  44264  smfresal  44333  smfres  44335  smfco  44347  fcoreslem1  44568  fcoreslem2  44569  fcores  44572  isomushgr  45289  ushrisomgr  45304  cnneiima  46221  sepfsepc  46232