Theorem ffund 6674

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

Syntax hints:   → wi 4  Fun wfun 6494  ⟶wf 6496

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 6503  df-f 6504

This theorem is referenced by:  fofun  6755  fssrescdmd  7081  fmptco  7084  funfvima2d  7188  smores2  8296  elmapfun  8815  fidmfisupp  9287  fdmfifsupp  9290  fsuppmptif  9314  fsuppco2  9318  fsuppcor  9319  ordtypelem8  9442  ordtypelem9  9443  ordtypelem10  9444  unxpwdom2  9505  fpwwe2  10566  swrdwrdsymb  14598  mrcuni  17556  frmdss2  18800  cntzmhm2  19283  frgpupval  19715  gsumzadd  19863  gsumpt  19903  gsum2dlem2  19912  dprd2da  19985  lmhmpreima  21012  lmhmlsp  21013  rhmpreimaidl  21244  cygznlem2  21535  frlmsslsp  21763  frlmup1  21765  frlmup4  21768  lindff1  21787  lindfrn  21788  psrelbasfun  21903  mvrcl  21959  evlslem3  22047  evlseu  22050  evlsvvvallem  22058  mpfind  22082  mhpmulcl  22104  psdmul  22121  gsumply1subr  22186  cnclsi  23228  cncnp  23236  paste  23250  connima  23381  1stcfb  23401  1stccnp  23418  1stckgenlem  23509  txcnpi  23564  txcnp  23576  xkoco2cn  23614  fmfnfmlem2  23911  lmflf  23961  txflf  23962  cnextcn  24023  clssubg  24065  ghmcnp  24071  metustid  24510  metustexhalf  24512  isngp2  24553  pi1xfrval  25022  pi1coval  25028  iscfil2  25234  rrxcph  25360  ismbfd  25608  ellimc2  25846  ellimc3  25848  dvres3  25882  dvres3a  25883  dvcnv  25949  dvcnvrelem1  25990  ftc1cn  26018  mdegldg  26039  plyeq0  26184  plyaddlem1  26186  plymullem1  26187  ulmdv  26380  dchrelbas2  27216  dchrghm  27235  uhgrfun  29151  vdegp1ai  29622  vdegp1bi  29623  wlkres  29754  sspg  30815  ssps  30817  sspn  30823  htthlem  31004  fmptcof2  32746  fnpreimac  32759  curry2ima  32798  offinsupp1  32815  fpwrelmapffslem  32821  indfsd  32960  swrdrn2  33046  pwrssmgc  33092  gsumhashmul  33160  xrge0tsmsd  33166  wrdpmtrlast  33186  cyc3co2  33233  tocyccntz  33237  rmfsupp2  33331  elrgspnlem1  33335  elrgspnlem2  33336  elrgspnlem3  33337  elrgspnlem4  33338  elrgspnsubrunlem1  33340  elrgspnsubrunlem2  33341  elrspunidl  33520  rhmimaidl  33524  ig1pmindeg  33694  extvfvcl  33712  mplmulmvr  33715  evlextv  33718  psrmonprod  33728  esplylem  33742  esplympl  33743  esplymhp  33744  esplyfv1  33745  ply1degltdimlem  33799  lbsdiflsp0  33803  fedgmullem1  33806  fedgmullem2  33807  evls1fldgencl  33847  fldextrspunlsp  33851  extdgfialglem1  33869  rhmpreimacnlem  34061  esumpfinvallem  34251  sibfof  34517  sitgclg  34519  eulerpartlemd  34543  eulerpartlemgu  34554  eulerpartlemgf  34556  dstrvprob  34649  dstfrvel  34651  orvclteinc  34653  spthcycl  35342  cvmliftmolem1  35494  cvmliftlem3  35500  cvmliftlem10  35507  cvmliftlem13  35509  cvmlift2lem9  35524  cvmlift3lem6  35537  cvmlift3lem7  35538  satefvfmla0  35631  satefvfmla1  35638  msubrn  35742  mclsax  35782  mclsppslem  35796  mclspps  35797  weiunfr  36680  ftc1cnnc  37940  heibor1lem  38057  grpokerinj  38141  aks6d1c3  42490  aks6d1c4  42491  sticksstones1  42513  aks6d1c6lem2  42538  rhmqusspan  42552  aks5lem2  42554  imacrhmcl  42881  evlselvlem  42941  evlselv  42942  lmhmfgima  43438  cantnfub  43675  onnoxpg  43782  gneispacefun  44490  relpfrlem  45306  cncmpmax  45389  limccog  45977  limsuppnfdlem  46056  climxrrelem  46104  climxrre  46105  liminfvalxr  46138  liminflimsupxrre  46172  xlimxrre  46186  dvsinax  46268  fvvolioof  46344  fvvolicof  46346  dirkercncflem2  46459  fourierdlem82  46543  subsaliuncllem  46712  fge0iccico  46725  sge0sn  46734  sge0tsms  46735  sge0cl  46736  sge0f1o  46737  sge0isum  46782  ovnovollem1  47011  ovnovollem2  47012  preimaioomnf  47074  smfresal  47143  smfres  47145  smfco  47157  fcoreslem1  47420  fcoreslem2  47421  fcores  47424  gricushgr  48274  ushggricedg  48284  uspgrlimlem4  48348  ffvbr  49212  cnneiima  49273  sepfsepc  49284  imaf1co  49511