Theorem ffund 6706

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6525  ⟶wf 6527

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 6534  df-f 6535

This theorem is used by:  fofun  6789  fssrescdmd  7119  fmptco  7122  funfvima2d  7230  smores2  8346  elmapfun  8872  fidmfisupp  9348  fdmfifsupp  9351  fsuppmptif  9375  fsuppco2  9379  fsuppcor  9380  ordtypelem8  9503  ordtypelem9  9504  ordtypelem10  9505  unxpwdom2  9566  fpwwe2  10709  swrdwrdsymb  14792  mrcuni  17775  frmdss2  19039  cntzmhm2  19536  frgpupval  19968  gsumzadd  20116  gsumpt  20156  gsum2dlem2  20165  dprd2da  20238  lmhmpreima  21303  lmhmlsp  21304  rhmpreimaidl  21551  cygznlem2  21854  frlmsslsp  22082  frlmup1  22084  frlmup4  22087  lindff1  22106  lindfrn  22107  psrelbasfun  22224  mvrcl  22279  evlslem3  22369  evlseu  22372  evlsvvvallem  22380  mpfind  22404  mhpmulcl  22450  psdmul  22467  gsumply1subr  22531  cnclsi  23570  cncnp  23578  paste  23592  connima  23723  1stcfb  23743  1stccnp  23761  1stckgenlem  23852  txcnpi  23907  txcnp  23919  xkoco2cn  23957  fmfnfmlem2  24254  lmflf  24304  txflf  24305  cnextcn  24366  clssubg  24408  ghmcnp  24414  metustid  24853  metustexhalf  24855  isngp2  24896  pi1xfrval  25355  pi1coval  25361  iscfil2  25567  rrxcph  25693  ismbfd  25940  ellimc2  26177  ellimc3  26179  dvres3  26213  dvres3a  26214  dvcnv  26277  dvcnvrelem1  26317  ftc1cn  26343  mdegldg  26364  plyeq0  26510  plyaddlem1  26512  plymullem1  26513  rnplynfin  26612  plyconz  26613  ulmdv  26712  dchrelbas2  27546  dchrghm  27565  uhgrfun  29626  vdegp1ai  30099  vdegp1bi  30100  wlkres  30231  spthcycl  30374  sspg  31312  ssps  31314  sspn  31320  htthlem  31501  fmptcof2  33233  fnpreimac  33246  curry2ima  33284  offinsupp1  33300  fpwrelmapffslem  33306  indfsd  33417  swrdrn2  33499  pwrssmgc  33543  gsumhashmul  33610  xrge0tsmsd  33616  wrdpmtrlast  33636  cyc3co2  33683  tocyccntz  33687  rmfsupp2  33780  elrgspnlem1  33785  elrgspnlem2  33786  elrgspnlem3  33787  elrgspnlem4  33788  elrgspnsubrunlem1  33790  elrgspnsubrunlem2  33791  elrspunidl  33960  rhmimaidl  33964  ig1pmindeg  34116  selvascl  34131  extvfvcl  34150  mplmulmvr  34153  evlextv  34156  psrmonprod  34166  esplylem  34180  esplympl  34181  esplymhp  34182  esplyfv1  34183  ply1degltdimlem  34236  lbsdiflsp0  34240  fedgmullem1  34243  fedgmullem2  34244  evls1fldgencl  34284  fldextrspunlsp  34288  extdgfialglem1  34306  rhmpreimacnlem  34498  esumpfinvallem  34688  sibfof  34955  sitgclg  34957  eulerpartlemd  34981  eulerpartlemgu  34992  eulerpartlemgf  34994  dstrvprob  35087  dstfrvel  35089  orvclteinc  35091  cvmliftmolem1  36015  cvmliftlem3  36021  cvmliftlem10  36028  cvmliftlem13  36030  cvmlift2lem9  36045  cvmlift3lem6  36058  cvmlift3lem7  36059  satefvfmla0  36152  satefvfmla1  36159  msubrn  36263  mclsax  36303  mclsppslem  36317  mclspps  36318  weiunfr  37225  ftc1cnnc  38578  heibor1lem  38711  grpokerinj  38795  aks6d1c3  43141  aks6d1c4  43142  sticksstones1  43164  aks6d1c6lem2  43189  rhmqusspan  43203  aks5lem2  43205  imacrhmcl  43546  evlselvlem  43578  evlselv  43579  lmhmfgima  44044  cantnfub  44281  onnoxpg  44388  gneispacefun  45096  relpfrlem  45895  cncmpmax  45992  limccog  46576  limsuppnfdlem  46655  climxrrelem  46703  climxrre  46704  liminfvalxr  46737  liminflimsupxrre  46771  xlimxrre  46785  dvsinax  46867  fvvolioof  46943  fvvolicof  46945  dirkercncflem2  47058  fourierdlem82  47142  fourierdlem113  47173  subsaliuncllem  47311  fge0iccico  47324  sge0sn  47333  sge0tsms  47334  sge0cl  47335  sge0f1o  47336  sge0isum  47381  ovnovollem1  47610  ovnovollem2  47611  preimaioomnf  47673  smfresal  47742  smfres  47744  smfco  47756  tmachlem-agreesn  47901  fcoreslem1  48077  fcoreslem2  48078  fcores  48081  gricushgr  48959  ushggricedg  48969  uspgrlimlem4  49033  ffvbr  49910  cnneiima  49969  sepfsepc  49980  imaf1co  50207