Theorem ffun 6048

Description: A mapping is a function. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
ffun	⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)

Proof of Theorem ffun

Step	Hyp	Ref	Expression
1		ffn 6045	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfun 5988	. 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 5882   Fn wfn 5883  ⟶wf 5884

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 197  df-an 386  df-fn 5891  df-f 5892

This theorem is referenced by:  ffund  6049  funssxp  6061  f00  6087  fimacnv  6347  dff3  6372  fliftf  6565  fun11iun  7126  frnsuppeq  7307  smores2  7451  pmfun  7877  elmapfun  7881  pmresg  7885  fodomr  8111  ac6sfi  8204  fissuni  8271  fipreima  8272  fdmfifsupp  8285  frnfsuppbi  8304  fsuppmptif  8305  fsuppco2  8308  fsuppcor  8309  ordtypelem8  8430  ordtypelem9  8431  ordtypelem10  8432  unxpwdom2  8493  cnfcomlem  8596  tcrank  8747  fseqenlem2  8848  carduniima  8919  infmap2  9040  hsmexlem4  9251  hsmexlem5  9252  axdc3lem2  9273  axdc3lem4  9275  smobeth  9408  fpwwe2lem13  9464  fpwwe2  9465  inar1  9597  grur1  9642  nqerid  9755  zexALT  11396  hashkf  13119  hashgval  13120  revco  13580  ccatco  13581  lswco  13584  climdm  14285  isercolllem2  14396  isercolllem3  14397  isercoll  14398  sum0  14452  sumz  14453  fsumsers  14459  isumclim  14488  ntrivcvgfvn0  14631  ntrivcvgtail  14632  zprodn0  14669  iprodclim  14729  znnen  14941  mrcuni  16281  isacs2  16314  isacs5  17172  cntzmhm2  17772  frgpupval  18187  gsumzadd  18322  gsumpt  18361  gsum2dlem2  18370  dprdss  18428  dprd2dlem1  18440  dprd2da  18441  dmdprdsplit2lem  18444  lmhmpreima  19048  lmhmlsp  19049  psrelbasfun  19380  mvrcl  19449  evlseu  19516  mpfind  19536  gsumply1subr  19604  cygznlem2  19917  frlmup1  20137  frlmup4  20140  lindff1  20159  lindfrn  20160  iscnp3  21048  subbascn  21058  cnpnei  21068  cnclima  21072  iscncl  21073  cnclsi  21076  cncls  21078  cncnp  21084  cnrest2  21090  paste  21098  cnhaus  21158  connima  21228  1stcfb  21248  1stccnp  21265  1stckgenlem  21356  kgencn3  21361  txcnpi  21411  txcnp  21423  xkopt  21458  xkoco2cn  21461  xkococnlem  21462  hmeores  21574  fbasrn  21688  uzrest  21701  rnelfmlem  21756  rnelfm  21757  fmfnfmlem2  21759  fmfnfmlem3  21760  fmfnfmlem4  21761  fmfnfm  21762  cnflf2  21807  lmflf  21809  txflf  21810  cnextcn  21871  clssubg  21912  ghmcnp  21918  metcnp  22346  metustid  22359  metustsym  22360  metustexhalf  22361  cfilucfil  22364  restmetu  22375  isngp2  22401  qtopbaslem  22562  tgqioo  22603  re2ndc  22604  bndth  22757  pi1xfrval  22854  pi1coval  22860  tchcph  23036  iscfil2  23064  rrxcph  23180  ovolficcss  23238  volf  23297  volsup  23324  uniioombllem3a  23352  uniioombllem4  23354  uniioombllem5  23355  dyadmbllem  23367  dyadmbl  23368  opnmbllem  23369  opnmblALT  23371  mbfimaicc  23400  ismbfd  23407  ismbf3d  23421  mbfimaopnlem  23422  mbfimaopn2  23424  i1fima  23445  i1fima2  23446  i1fd  23448  itg1addlem4  23466  ellimc2  23641  ellimc3  23643  dvres3  23677  dvres3a  23678  dvidlem  23679  dvcnp  23682  dvadd  23703  dvmul  23704  dvaddf  23705  dvmulf  23706  dvco  23710  dvcof  23711  dvcjbr  23712  dvcj  23713  dvrec  23718  dvcnvlem  23739  dvcnv  23740  dvef  23743  dvferm1  23748  dvferm2  23750  c1liplem1  23759  dvcnvrelem1  23780  dvcnvrelem2  23781  ftc1cn  23806  mdegcl  23829  deg1n0ima  23849  plyco0  23948  plyeq0  23967  plypf1  23968  plyaddlem1  23969  plymullem1  23970  tayl0  24116  ulmdvlem3  24156  ulmdv  24157  pserdv  24183  dvlog  24397  efopn  24404  relogbf  24529  dchrelbas2  24962  dchrghm  24981  subusgr  26181  vdegp1ai  26432  wlkreslem  26566  pthdivtx  26625  pthdlem2lem  26663  sspg  27583  ssps  27585  sspn  27591  htthlem  27774  issh2  28066  hlimuni  28095  hhsscms  28136  occllem  28162  occl  28163  chscllem4  28499  imaelshi  28917  fmptcof2  29457  curry2ima  29486  fpwrelmapffslem  29507  xrofsup  29533  xrge0tsmsd  29785  smatrcl  29862  mdetpmtr1  29889  locfinreflem  29907  fsumcvg4  29996  zrhunitpreima  30022  esumpfinvallem  30136  imambfm  30324  carsggect  30380  sibfof  30402  sitgclg  30404  eulerpartlemd  30428  eulerpartlemt  30433  eulerpartlemmf  30437  eulerpartlemgvv  30438  eulerpartlemgu  30439  eulerpartlemgf  30441  dstrvprob  30533  dstfrvel  30535  orvclteinc  30537  rpsqrtcn  30671  erdszelem2  31174  erdszelem7  31179  erdszelem8  31180  cvmliftmolem1  31263  cvmliftlem3  31269  cvmliftlem10  31276  cvmliftlem13  31278  cvmliftlem15  31280  cvmlift2lem9  31293  cvmlift3lem6  31306  cvmlift3lem7  31307  mrsub0  31413  mrsubccat  31415  mrsubcn  31416  msubrn  31426  mclsax  31466  mthmblem  31477  mclsppslem  31480  mclspps  31481  nofun  31802  madeval  31935  ivthALT  32330  icoreunrn  33207  icoreelrn  33209  curf  33387  curunc  33391  heicant  33444  opnmbllem0  33445  mblfinlem1  33446  itg2addnclem  33461  itg2addnclem2  33462  ftc1cnnc  33484  ftc1anclem7  33491  ftc1anc  33493  ftc2nc  33494  indexdom  33529  cnres2  33562  heibor1lem  33608  grpokerinj  33692  elrfirn  37258  fnwe2lem2  37621  lmhmfgima  37654  arearect  37801  areaquad  37802  funfvima2d  38469  cncmpmax  39191  fidmfisupp  39390  absfun  39566  evthiccabs  39718  ioofun  39778  limccog  39852  cncficcgt0  40101  dvsinax  40127  fperdvper  40133  fvvolioof  40206  fvvolicof  40208  dirkercncflem2  40321  fourierdlem20  40344  fourierdlem42  40366  fourierdlem63  40386  fourierdlem76  40399  fourierdlem82  40405  fourierdlem93  40416  fourierdlem97  40420  fourierdlem113  40436  fge0iccico  40587  sge0sn  40596  sge0tsms  40597  sge0cl  40598  sge0f1o  40599  sge0isum  40644  ovolval3  40861  ovnovollem1  40870  pfxco  41438  fmtnoinf  41448  elbigolo1  42351