Theorem ffund 6711

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6531  ⟶wf 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6540  df-f 6541

This theorem is used by:  fofun  6794  fssrescdmd  7124  fmptco  7127  funfvima2d  7235  smores2  8347  elmapfun  8871  fidmfisupp  9346  fdmfifsupp  9349  fsuppmptif  9373  fsuppco2  9377  fsuppcor  9378  ordtypelem8  9501  ordtypelem9  9502  ordtypelem10  9503  unxpwdom2  9564  fpwwe2  10656  swrdwrdsymb  14736  mrcuni  17715  frmdss2  18978  cntzmhm2  19475  frgpupval  19907  gsumzadd  20055  gsumpt  20095  gsum2dlem2  20104  dprd2da  20177  lmhmpreima  21238  lmhmlsp  21239  rhmpreimaidl  21485  cygznlem2  21787  frlmsslsp  22015  frlmup1  22017  frlmup4  22020  lindff1  22039  lindfrn  22040  psrelbasfun  22157  mvrcl  22212  evlslem3  22302  evlseu  22305  evlsvvvallem  22313  mpfind  22337  mhpmulcl  22383  psdmul  22400  gsumply1subr  22464  cnclsi  23503  cncnp  23511  paste  23525  connima  23656  1stcfb  23676  1stccnp  23694  1stckgenlem  23785  txcnpi  23840  txcnp  23852  xkoco2cn  23890  fmfnfmlem2  24187  lmflf  24237  txflf  24238  cnextcn  24299  clssubg  24341  ghmcnp  24347  metustid  24786  metustexhalf  24788  isngp2  24829  pi1xfrval  25288  pi1coval  25294  iscfil2  25500  rrxcph  25626  ismbfd  25873  ellimc2  26111  ellimc3  26113  dvres3  26147  dvres3a  26148  dvcnv  26211  dvcnvrelem1  26251  ftc1cn  26277  mdegldg  26298  plyeq0  26444  plyaddlem1  26446  plymullem1  26447  rnplynfin  26546  plyconz  26547  ulmdv  26646  dchrelbas2  27481  dchrghm  27500  uhgrfun  29531  vdegp1ai  30004  vdegp1bi  30005  wlkres  30136  spthcycl  30279  sspg  31217  ssps  31219  sspn  31225  htthlem  31406  fmptcof2  33138  fnpreimac  33151  curry2ima  33189  offinsupp1  33205  fpwrelmapffslem  33211  indfsd  33322  swrdrn2  33404  pwrssmgc  33448  gsumhashmul  33515  xrge0tsmsd  33521  wrdpmtrlast  33541  cyc3co2  33588  tocyccntz  33592  rmfsupp2  33685  elrgspnlem1  33690  elrgspnlem2  33691  elrgspnlem3  33692  elrgspnlem4  33693  elrgspnsubrunlem1  33695  elrgspnsubrunlem2  33696  elrspunidl  33864  rhmimaidl  33868  ig1pmindeg  34020  selvascl  34035  extvfvcl  34054  mplmulmvr  34057  evlextv  34060  psrmonprod  34070  esplylem  34084  esplympl  34085  esplymhp  34086  esplyfv1  34087  ply1degltdimlem  34140  lbsdiflsp0  34144  fedgmullem1  34147  fedgmullem2  34148  evls1fldgencl  34188  fldextrspunlsp  34192  extdgfialglem1  34210  rhmpreimacnlem  34402  esumpfinvallem  34592  sibfof  34859  sitgclg  34861  eulerpartlemd  34885  eulerpartlemgu  34896  eulerpartlemgf  34898  dstrvprob  34991  dstfrvel  34993  orvclteinc  34995  cvmliftmolem1  35868  cvmliftlem3  35874  cvmliftlem10  35881  cvmliftlem13  35883  cvmlift2lem9  35898  cvmlift3lem6  35911  cvmlift3lem7  35912  satefvfmla0  36005  satefvfmla1  36012  msubrn  36116  mclsax  36156  mclsppslem  36170  mclspps  36171  weiunfr  37094  ftc1cnnc  38449  heibor1lem  38567  grpokerinj  38651  aks6d1c3  42997  aks6d1c4  42998  sticksstones1  43020  aks6d1c6lem2  43045  rhmqusspan  43059  aks5lem2  43061  imacrhmcl  43410  evlselvlem  43442  evlselv  43443  lmhmfgima  43933  cantnfub  44170  onnoxpg  44277  gneispacefun  44985  relpfrlem  45784  cncmpmax  45874  limccog  46458  limsuppnfdlem  46537  climxrrelem  46585  climxrre  46586  liminfvalxr  46619  liminflimsupxrre  46653  xlimxrre  46667  dvsinax  46749  fvvolioof  46825  fvvolicof  46827  dirkercncflem2  46940  fourierdlem82  47024  fourierdlem113  47055  subsaliuncllem  47193  fge0iccico  47206  sge0sn  47215  sge0tsms  47216  sge0cl  47217  sge0f1o  47218  sge0isum  47263  ovnovollem1  47492  ovnovollem2  47493  preimaioomnf  47555  smfresal  47624  smfres  47626  smfco  47638  tmachlem-agreesn  47783  fcoreslem1  47959  fcoreslem2  47960  fcores  47963  gricushgr  48841  ushggricedg  48851  uspgrlimlem4  48915  ffvbr  49792  cnneiima  49851  sepfsepc  49862  imaf1co  50089