Theorem ffund 6722

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

Syntax hints:   → wi 4  Fun wfun 6538  ⟶wf 6540

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 395  df-fn 6547  df-f 6548

This theorem is referenced by:  fofun  6807  fmptco  7130  funfvima2d  7237  smores2  8358  elmapfun  8864  fidmfisupp  9375  fdmfifsupp  9377  fsuppmptif  9398  fsuppco2  9402  fsuppcor  9403  ordtypelem8  9524  ordtypelem9  9525  ordtypelem10  9526  unxpwdom2  9587  fpwwe2  10642  swrdwrdsymb  14618  mrcuni  17571  frmdss2  18782  cntzmhm2  19249  frgpupval  19685  gsumzadd  19833  gsumpt  19873  gsum2dlem2  19882  dprd2da  19955  lmhmpreima  20805  lmhmlsp  20806  cygznlem2  21345  frlmsslsp  21572  frlmup1  21574  frlmup4  21577  lindff1  21596  lindfrn  21597  psrelbasfun  21720  mvrcl  21772  evlslem3  21864  evlseu  21867  mpfind  21891  mhpmulcl  21913  gsumply1subr  21978  cnclsi  22998  cncnp  23006  paste  23020  connima  23151  1stcfb  23171  1stccnp  23188  1stckgenlem  23279  txcnpi  23334  txcnp  23346  xkoco2cn  23384  fmfnfmlem2  23681  lmflf  23731  txflf  23732  cnextcn  23793  clssubg  23835  ghmcnp  23841  metustid  24285  metustexhalf  24287  isngp2  24328  pi1xfrval  24803  pi1coval  24809  iscfil2  25016  rrxcph  25142  ismbfd  25390  ellimc2  25628  ellimc3  25630  dvres3  25664  dvres3a  25665  dvcnv  25728  dvcnvrelem1  25768  ftc1cn  25794  mdegldg  25818  plyeq0  25959  plyaddlem1  25961  plymullem1  25962  ulmdv  26149  dchrelbas2  26974  dchrghm  26993  uhgrfun  28591  vdegp1ai  29058  vdegp1bi  29059  wlkres  29192  sspg  30246  ssps  30248  sspn  30254  htthlem  30435  fmptcof2  32147  fnpreimac  32161  curry2ima  32195  offinsupp1  32217  fpwrelmapffslem  32222  swrdrn2  32383  pwrssmgc  32435  gsumhashmul  32476  xrge0tsmsd  32477  cyc3co2  32567  tocyccntz  32571  rmfsupp2  32655  rhmpreimaidl  32809  elrspunidl  32818  rhmimaidl  32822  ig1pmindeg  32945  ply1degltdimlem  32993  lbsdiflsp0  32997  fedgmullem1  33000  fedgmullem2  33001  evls1fldgencl  33031  rhmpreimacnlem  33160  esumpfinvallem  33368  sibfof  33635  sitgclg  33637  eulerpartlemd  33661  eulerpartlemgu  33672  eulerpartlemgf  33674  dstrvprob  33766  dstfrvel  33768  orvclteinc  33770  spthcycl  34416  cvmliftmolem1  34568  cvmliftlem3  34574  cvmliftlem10  34581  cvmliftlem13  34583  cvmlift2lem9  34598  cvmlift3lem6  34611  cvmlift3lem7  34612  satefvfmla0  34705  satefvfmla1  34712  msubrn  34816  mclsax  34856  mclsppslem  34870  mclspps  34871  ftc1cnnc  36865  heibor1lem  36982  grpokerinj  37066  sticksstones1  41270  imacrhmcl  41395  evlsvvvallem  41437  evlselvlem  41462  evlselv  41463  lmhmfgima  42130  cantnfub  42375  onnog  42484  gneispacefun  43192  cncmpmax  44020  limccog  44636  limsuppnfdlem  44717  climxrrelem  44765  climxrre  44766  liminfvalxr  44799  liminflimsupxrre  44833  xlimxrre  44847  dvsinax  44929  fvvolioof  45005  fvvolicof  45007  dirkercncflem2  45120  fourierdlem82  45204  subsaliuncllem  45373  fge0iccico  45386  sge0sn  45395  sge0tsms  45396  sge0cl  45397  sge0f1o  45398  sge0isum  45443  ovnovollem1  45672  ovnovollem2  45673  preimaioomnf  45735  smfresal  45804  smfres  45806  smfco  45818  fcoreslem1  46073  fcoreslem2  46074  fcores  46077  isomushgr  46794  ushrisomgr  46809  cnneiima  47638  sepfsepc  47649