Theorem ffund 6655

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 6654	. 2 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)
3	1, 2	syl 17	1 ⊢ (𝜑 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 6475  ⟶wf 6477

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 207  df-an 396  df-fn 6484  df-f 6485

This theorem is referenced by:  fofun  6736  fssrescdmd  7059  fmptco  7062  funfvima2d  7166  smores2  8274  elmapfun  8790  fidmfisupp  9256  fdmfifsupp  9259  fsuppmptif  9283  fsuppco2  9287  fsuppcor  9288  ordtypelem8  9411  ordtypelem9  9412  ordtypelem10  9413  unxpwdom2  9474  fpwwe2  10534  swrdwrdsymb  14570  mrcuni  17527  frmdss2  18771  cntzmhm2  19255  frgpupval  19687  gsumzadd  19835  gsumpt  19875  gsum2dlem2  19884  dprd2da  19957  lmhmpreima  20983  lmhmlsp  20984  rhmpreimaidl  21215  cygznlem2  21506  frlmsslsp  21734  frlmup1  21736  frlmup4  21739  lindff1  21758  lindfrn  21759  psrelbasfun  21873  mvrcl  21930  evlslem3  22016  evlseu  22019  mpfind  22043  mhpmulcl  22065  psdmul  22082  gsumply1subr  22147  cnclsi  23188  cncnp  23196  paste  23210  connima  23341  1stcfb  23361  1stccnp  23378  1stckgenlem  23469  txcnpi  23524  txcnp  23536  xkoco2cn  23574  fmfnfmlem2  23871  lmflf  23921  txflf  23922  cnextcn  23983  clssubg  24025  ghmcnp  24031  metustid  24470  metustexhalf  24472  isngp2  24513  pi1xfrval  24982  pi1coval  24988  iscfil2  25194  rrxcph  25320  ismbfd  25568  ellimc2  25806  ellimc3  25808  dvres3  25842  dvres3a  25843  dvcnv  25909  dvcnvrelem1  25950  ftc1cn  25978  mdegldg  25999  plyeq0  26144  plyaddlem1  26146  plymullem1  26147  ulmdv  26340  dchrelbas2  27176  dchrghm  27195  uhgrfun  29045  vdegp1ai  29516  vdegp1bi  29517  wlkres  29648  sspg  30706  ssps  30708  sspn  30714  htthlem  30895  fmptcof2  32637  fnpreimac  32651  curry2ima  32688  offinsupp1  32707  fpwrelmapffslem  32713  indfsd  32847  swrdrn2  32933  pwrssmgc  32979  gsumhashmul  33039  xrge0tsmsd  33040  wrdpmtrlast  33060  cyc3co2  33107  tocyccntz  33111  rmfsupp2  33203  elrgspnlem1  33207  elrgspnlem2  33208  elrgspnlem3  33209  elrgspnlem4  33210  elrgspnsubrunlem1  33212  elrgspnsubrunlem2  33213  elrspunidl  33391  rhmimaidl  33395  ig1pmindeg  33560  esplylem  33585  esplympl  33586  esplymhp  33587  esplyfv1  33588  ply1degltdimlem  33633  lbsdiflsp0  33637  fedgmullem1  33640  fedgmullem2  33641  evls1fldgencl  33681  fldextrspunlsp  33685  extdgfialglem1  33703  rhmpreimacnlem  33895  esumpfinvallem  34085  sibfof  34351  sitgclg  34353  eulerpartlemd  34377  eulerpartlemgu  34388  eulerpartlemgf  34390  dstrvprob  34483  dstfrvel  34485  orvclteinc  34487  spthcycl  35171  cvmliftmolem1  35323  cvmliftlem3  35329  cvmliftlem10  35336  cvmliftlem13  35338  cvmlift2lem9  35353  cvmlift3lem6  35366  cvmlift3lem7  35367  satefvfmla0  35460  satefvfmla1  35467  msubrn  35571  mclsax  35611  mclsppslem  35625  mclspps  35626  weiunfr  36507  ftc1cnnc  37738  heibor1lem  37855  grpokerinj  37939  aks6d1c3  42162  aks6d1c4  42163  sticksstones1  42185  aks6d1c6lem2  42210  rhmqusspan  42224  aks5lem2  42226  imacrhmcl  42553  evlsvvvallem  42600  evlselvlem  42625  evlselv  42626  lmhmfgima  43123  cantnfub  43360  onnog  43468  gneispacefun  44176  relpfrlem  44992  cncmpmax  45075  limccog  45666  limsuppnfdlem  45745  climxrrelem  45793  climxrre  45794  liminfvalxr  45827  liminflimsupxrre  45861  xlimxrre  45875  dvsinax  45957  fvvolioof  46033  fvvolicof  46035  dirkercncflem2  46148  fourierdlem82  46232  subsaliuncllem  46401  fge0iccico  46414  sge0sn  46423  sge0tsms  46424  sge0cl  46425  sge0f1o  46426  sge0isum  46471  ovnovollem1  46700  ovnovollem2  46701  preimaioomnf  46763  smfresal  46832  smfres  46834  smfco  46846  fcoreslem1  47100  fcoreslem2  47101  fcores  47104  gricushgr  47954  ushggricedg  47964  uspgrlimlem4  48028  ffvbr  48893  cnneiima  48954  sepfsepc  48965  imaf1co  49193