Theorem ffund 6718

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

Syntax hints:   → wi 4  Fun wfun 6534  ⟶wf 6536

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 6543  df-f 6544

This theorem is referenced by:  fofun  6803  fmptco  7123  funfvima2d  7230  smores2  8350  elmapfun  8856  fidmfisupp  9367  fdmfifsupp  9369  fsuppmptif  9390  fsuppco2  9394  fsuppcor  9395  ordtypelem8  9516  ordtypelem9  9517  ordtypelem10  9518  unxpwdom2  9579  fpwwe2  10634  swrdwrdsymb  14608  mrcuni  17561  frmdss2  18740  cntzmhm2  19200  frgpupval  19636  gsumzadd  19784  gsumpt  19824  gsum2dlem2  19833  dprd2da  19906  lmhmpreima  20651  lmhmlsp  20652  cygznlem2  21115  frlmsslsp  21342  frlmup1  21344  frlmup4  21347  lindff1  21366  lindfrn  21367  psrelbasfun  21490  mvrcl  21542  evlslem3  21634  evlseu  21637  mpfind  21661  mhpmulcl  21683  gsumply1subr  21747  cnclsi  22767  cncnp  22775  paste  22789  connima  22920  1stcfb  22940  1stccnp  22957  1stckgenlem  23048  txcnpi  23103  txcnp  23115  xkoco2cn  23153  fmfnfmlem2  23450  lmflf  23500  txflf  23501  cnextcn  23562  clssubg  23604  ghmcnp  23610  metustid  24054  metustexhalf  24056  isngp2  24097  pi1xfrval  24561  pi1coval  24567  iscfil2  24774  rrxcph  24900  ismbfd  25147  ellimc2  25385  ellimc3  25387  dvres3  25421  dvres3a  25422  dvcnv  25485  dvcnvrelem1  25525  ftc1cn  25551  mdegldg  25575  plyeq0  25716  plyaddlem1  25718  plymullem1  25719  ulmdv  25906  dchrelbas2  26729  dchrghm  26748  uhgrfun  28315  vdegp1ai  28782  vdegp1bi  28783  wlkres  28916  sspg  29968  ssps  29970  sspn  29976  htthlem  30157  fmptcof2  31869  fnpreimac  31883  curry2ima  31917  offinsupp1  31939  fpwrelmapffslem  31944  swrdrn2  32105  pwrssmgc  32157  gsumhashmul  32195  xrge0tsmsd  32196  cyc3co2  32286  tocyccntz  32290  rmfsupp2  32375  rhmpreimaidl  32525  elrspunidl  32534  rhmimaidl  32538  ig1pmindeg  32659  ply1degltdimlem  32695  lbsdiflsp0  32699  fedgmullem1  32702  fedgmullem2  32703  rhmpreimacnlem  32852  esumpfinvallem  33060  sibfof  33327  sitgclg  33329  eulerpartlemd  33353  eulerpartlemgu  33364  eulerpartlemgf  33366  dstrvprob  33458  dstfrvel  33460  orvclteinc  33462  spthcycl  34108  cvmliftmolem1  34260  cvmliftlem3  34266  cvmliftlem10  34273  cvmliftlem13  34275  cvmlift2lem9  34290  cvmlift3lem6  34303  cvmlift3lem7  34304  satefvfmla0  34397  satefvfmla1  34404  msubrn  34508  mclsax  34548  mclsppslem  34562  mclspps  34563  ftc1cnnc  36548  heibor1lem  36665  grpokerinj  36749  sticksstones1  40950  imacrhmcl  41086  evlsvvvallem  41130  evlselvlem  41155  evlselv  41156  lmhmfgima  41811  cantnfub  42056  onnog  42165  gneispacefun  42873  cncmpmax  43701  limccog  44322  limsuppnfdlem  44403  climxrrelem  44451  climxrre  44452  liminfvalxr  44485  liminflimsupxrre  44519  xlimxrre  44533  dvsinax  44615  fvvolioof  44691  fvvolicof  44693  dirkercncflem2  44806  fourierdlem82  44890  subsaliuncllem  45059  fge0iccico  45072  sge0sn  45081  sge0tsms  45082  sge0cl  45083  sge0f1o  45084  sge0isum  45129  ovnovollem1  45358  ovnovollem2  45359  preimaioomnf  45421  smfresal  45490  smfres  45492  smfco  45504  fcoreslem1  45759  fcoreslem2  45760  fcores  45763  isomushgr  46480  ushrisomgr  46495  cnneiima  47502  sepfsepc  47513