Theorem ffund 6692

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

Syntax hints:   → wi 4  Fun wfun 6505  ⟶wf 6507

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 6514  df-f 6515

This theorem is referenced by:  fofun  6773  fssrescdmd  7098  fmptco  7101  funfvima2d  7206  smores2  8323  elmapfun  8839  fidmfisupp  9323  fdmfifsupp  9326  fsuppmptif  9350  fsuppco2  9354  fsuppcor  9355  ordtypelem8  9478  ordtypelem9  9479  ordtypelem10  9480  unxpwdom2  9541  fpwwe2  10596  swrdwrdsymb  14627  mrcuni  17582  frmdss2  18790  cntzmhm2  19274  frgpupval  19704  gsumzadd  19852  gsumpt  19892  gsum2dlem2  19901  dprd2da  19974  lmhmpreima  20955  lmhmlsp  20956  rhmpreimaidl  21187  cygznlem2  21478  frlmsslsp  21705  frlmup1  21707  frlmup4  21710  lindff1  21729  lindfrn  21730  psrelbasfun  21844  mvrcl  21901  evlslem3  21987  evlseu  21990  mpfind  22014  mhpmulcl  22036  psdmul  22053  gsumply1subr  22118  cnclsi  23159  cncnp  23167  paste  23181  connima  23312  1stcfb  23332  1stccnp  23349  1stckgenlem  23440  txcnpi  23495  txcnp  23507  xkoco2cn  23545  fmfnfmlem2  23842  lmflf  23892  txflf  23893  cnextcn  23954  clssubg  23996  ghmcnp  24002  metustid  24442  metustexhalf  24444  isngp2  24485  pi1xfrval  24954  pi1coval  24960  iscfil2  25166  rrxcph  25292  ismbfd  25540  ellimc2  25778  ellimc3  25780  dvres3  25814  dvres3a  25815  dvcnv  25881  dvcnvrelem1  25922  ftc1cn  25950  mdegldg  25971  plyeq0  26116  plyaddlem1  26118  plymullem1  26119  ulmdv  26312  dchrelbas2  27148  dchrghm  27167  uhgrfun  28993  vdegp1ai  29464  vdegp1bi  29465  wlkres  29598  sspg  30657  ssps  30659  sspn  30665  htthlem  30846  fmptcof2  32581  fnpreimac  32595  curry2ima  32632  offinsupp1  32650  fpwrelmapffslem  32655  swrdrn2  32876  pwrssmgc  32926  gsumhashmul  33001  xrge0tsmsd  33002  wrdpmtrlast  33050  cyc3co2  33097  tocyccntz  33101  rmfsupp2  33189  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem3  33195  elrgspnlem4  33196  elrgspnsubrunlem1  33198  elrgspnsubrunlem2  33199  elrspunidl  33399  rhmimaidl  33403  ig1pmindeg  33567  ply1degltdimlem  33618  lbsdiflsp0  33622  fedgmullem1  33625  fedgmullem2  33626  evls1fldgencl  33665  fldextrspunlsp  33669  rhmpreimacnlem  33874  esumpfinvallem  34064  sibfof  34331  sitgclg  34333  eulerpartlemd  34357  eulerpartlemgu  34368  eulerpartlemgf  34370  dstrvprob  34463  dstfrvel  34465  orvclteinc  34467  spthcycl  35116  cvmliftmolem1  35268  cvmliftlem3  35274  cvmliftlem10  35281  cvmliftlem13  35283  cvmlift2lem9  35298  cvmlift3lem6  35311  cvmlift3lem7  35312  satefvfmla0  35405  satefvfmla1  35412  msubrn  35516  mclsax  35556  mclsppslem  35570  mclspps  35571  weiunfr  36455  ftc1cnnc  37686  heibor1lem  37803  grpokerinj  37887  aks6d1c3  42111  aks6d1c4  42112  sticksstones1  42134  aks6d1c6lem2  42159  rhmqusspan  42173  aks5lem2  42175  imacrhmcl  42502  evlsvvvallem  42549  evlselvlem  42574  evlselv  42575  lmhmfgima  43073  cantnfub  43310  onnog  43418  gneispacefun  44126  relpfrlem  44943  cncmpmax  45026  limccog  45618  limsuppnfdlem  45699  climxrrelem  45747  climxrre  45748  liminfvalxr  45781  liminflimsupxrre  45815  xlimxrre  45829  dvsinax  45911  fvvolioof  45987  fvvolicof  45989  dirkercncflem2  46102  fourierdlem82  46186  subsaliuncllem  46355  fge0iccico  46368  sge0sn  46377  sge0tsms  46378  sge0cl  46379  sge0f1o  46380  sge0isum  46425  ovnovollem1  46654  ovnovollem2  46655  preimaioomnf  46717  smfresal  46786  smfres  46788  smfco  46800  fcoreslem1  47064  fcoreslem2  47065  fcores  47068  gricushgr  47917  ushggricedg  47927  uspgrlimlem4  47990  ffvbr  48844  cnneiima  48905  sepfsepc  48916  imaf1co  49144