Theorem ffund 6695

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

Syntax hints:   → wi 4  Fun wfun 6508  ⟶wf 6510

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 6517  df-f 6518

This theorem is referenced by:  fofun  6776  fssrescdmd  7101  fmptco  7104  funfvima2d  7209  smores2  8326  elmapfun  8842  fidmfisupp  9330  fdmfifsupp  9333  fsuppmptif  9357  fsuppco2  9361  fsuppcor  9362  ordtypelem8  9485  ordtypelem9  9486  ordtypelem10  9487  unxpwdom2  9548  fpwwe2  10603  swrdwrdsymb  14634  mrcuni  17589  frmdss2  18797  cntzmhm2  19281  frgpupval  19711  gsumzadd  19859  gsumpt  19899  gsum2dlem2  19908  dprd2da  19981  lmhmpreima  20962  lmhmlsp  20963  rhmpreimaidl  21194  cygznlem2  21485  frlmsslsp  21712  frlmup1  21714  frlmup4  21717  lindff1  21736  lindfrn  21737  psrelbasfun  21851  mvrcl  21908  evlslem3  21994  evlseu  21997  mpfind  22021  mhpmulcl  22043  psdmul  22060  gsumply1subr  22125  cnclsi  23166  cncnp  23174  paste  23188  connima  23319  1stcfb  23339  1stccnp  23356  1stckgenlem  23447  txcnpi  23502  txcnp  23514  xkoco2cn  23552  fmfnfmlem2  23849  lmflf  23899  txflf  23900  cnextcn  23961  clssubg  24003  ghmcnp  24009  metustid  24449  metustexhalf  24451  isngp2  24492  pi1xfrval  24961  pi1coval  24967  iscfil2  25173  rrxcph  25299  ismbfd  25547  ellimc2  25785  ellimc3  25787  dvres3  25821  dvres3a  25822  dvcnv  25888  dvcnvrelem1  25929  ftc1cn  25957  mdegldg  25978  plyeq0  26123  plyaddlem1  26125  plymullem1  26126  ulmdv  26319  dchrelbas2  27155  dchrghm  27174  uhgrfun  29000  vdegp1ai  29471  vdegp1bi  29472  wlkres  29605  sspg  30664  ssps  30666  sspn  30672  htthlem  30853  fmptcof2  32588  fnpreimac  32602  curry2ima  32639  offinsupp1  32657  fpwrelmapffslem  32662  swrdrn2  32883  pwrssmgc  32933  gsumhashmul  33008  xrge0tsmsd  33009  wrdpmtrlast  33057  cyc3co2  33104  tocyccntz  33108  rmfsupp2  33196  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem3  33202  elrgspnlem4  33203  elrgspnsubrunlem1  33205  elrgspnsubrunlem2  33206  elrspunidl  33406  rhmimaidl  33410  ig1pmindeg  33574  ply1degltdimlem  33625  lbsdiflsp0  33629  fedgmullem1  33632  fedgmullem2  33633  evls1fldgencl  33672  fldextrspunlsp  33676  rhmpreimacnlem  33881  esumpfinvallem  34071  sibfof  34338  sitgclg  34340  eulerpartlemd  34364  eulerpartlemgu  34375  eulerpartlemgf  34377  dstrvprob  34470  dstfrvel  34472  orvclteinc  34474  spthcycl  35123  cvmliftmolem1  35275  cvmliftlem3  35281  cvmliftlem10  35288  cvmliftlem13  35290  cvmlift2lem9  35305  cvmlift3lem6  35318  cvmlift3lem7  35319  satefvfmla0  35412  satefvfmla1  35419  msubrn  35523  mclsax  35563  mclsppslem  35577  mclspps  35578  weiunfr  36462  ftc1cnnc  37693  heibor1lem  37810  grpokerinj  37894  aks6d1c3  42118  aks6d1c4  42119  sticksstones1  42141  aks6d1c6lem2  42166  rhmqusspan  42180  aks5lem2  42182  imacrhmcl  42509  evlsvvvallem  42556  evlselvlem  42581  evlselv  42582  lmhmfgima  43080  cantnfub  43317  onnog  43425  gneispacefun  44133  relpfrlem  44950  cncmpmax  45033  limccog  45625  limsuppnfdlem  45706  climxrrelem  45754  climxrre  45755  liminfvalxr  45788  liminflimsupxrre  45822  xlimxrre  45836  dvsinax  45918  fvvolioof  45994  fvvolicof  45996  dirkercncflem2  46109  fourierdlem82  46193  subsaliuncllem  46362  fge0iccico  46375  sge0sn  46384  sge0tsms  46385  sge0cl  46386  sge0f1o  46387  sge0isum  46432  ovnovollem1  46661  ovnovollem2  46662  preimaioomnf  46724  smfresal  46793  smfres  46795  smfco  46807  fcoreslem1  47068  fcoreslem2  47069  fcores  47072  gricushgr  47921  ushggricedg  47931  uspgrlimlem4  47994  ffvbr  48848  cnneiima  48909  sepfsepc  48920  imaf1co  49148