Theorem ffun 5961

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

Syntax hints:   → wi 4  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800

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 196  df-an 385  df-fn 5807  df-f 5808

This theorem is referenced by:  ffund  5962  funssxp  5974  f00  6000  fofun  6029  fimacnv  6255  dff3  6280  fliftf  6465  fun11iun  7019  frnsuppeq  7194  smores2  7338  pmfun  7763  elmapfun  7767  pmresg  7771  fodomr  7996  ac6sfi  8089  fissuni  8154  fipreima  8155  fdmfifsupp  8168  frnfsuppbi  8187  fsuppmptif  8188  fsuppco2  8191  fsuppcor  8192  ordtypelem8  8313  ordtypelem9  8314  ordtypelem10  8315  unxpwdom2  8376  cnfcomlem  8479  tcrank  8630  fseqenlem2  8731  carduniima  8802  infmap2  8923  hsmexlem4  9134  hsmexlem5  9135  axdc3lem2  9156  axdc3lem4  9158  smobeth  9287  fpwwe2lem13  9343  fpwwe2  9344  inar1  9476  grur1  9521  nqerid  9634  zexALT  11273  hashkf  12981  hashgval  12982  revco  13431  ccatco  13432  lswco  13435  climdm  14133  isercolllem2  14244  isercolllem3  14245  isercoll  14246  sum0  14299  sumz  14300  fsumsers  14306  isumclim  14330  ntrivcvgfvn0  14470  ntrivcvgtail  14471  zprodn0  14508  iprodclim  14568  znnen  14780  mrcuni  16104  isacs2  16137  isacs5  16995  cntzmhm2  17595  frgpupval  18010  gsumzadd  18145  gsumpt  18184  gsum2dlem2  18193  dprdss  18251  dprd2dlem1  18263  dprd2da  18264  dmdprdsplit2lem  18267  lmhmpreima  18869  lmhmlsp  18870  psrelbasfun  19201  mvrcl  19270  evlseu  19337  mpfind  19357  gsumply1subr  19425  cygznlem2  19736  frlmup1  19956  frlmup4  19959  lindff1  19978  lindfrn  19979  iscnp3  20858  subbascn  20868  cnpnei  20878  cnclima  20882  iscncl  20883  cnclsi  20886  cncls  20888  cncnp  20894  cnrest2  20900  paste  20908  cnhaus  20968  conima  21038  1stcfb  21058  1stccnp  21075  1stckgenlem  21166  kgencn3  21171  txcnpi  21221  txcnp  21233  xkopt  21268  xkoco2cn  21271  xkococnlem  21272  hmeores  21384  fbasrn  21498  uzrest  21511  rnelfmlem  21566  rnelfm  21567  fmfnfmlem2  21569  fmfnfmlem3  21570  fmfnfmlem4  21571  fmfnfm  21572  cnflf2  21617  lmflf  21619  txflf  21620  cnextcn  21681  clssubg  21722  ghmcnp  21728  metcnp  22156  metustid  22169  metustsym  22170  metustexhalf  22171  cfilucfil  22174  restmetu  22185  isngp2  22211  qtopbaslem  22372  tgqioo  22411  re2ndc  22412  bndth  22565  pi1xfrval  22662  pi1coval  22668  tchcph  22844  iscfil2  22872  rrxcph  22988  ovolficcss  23045  volf  23104  volsup  23131  uniioombllem3a  23158  uniioombllem4  23160  uniioombllem5  23161  dyadmbllem  23173  dyadmbl  23174  opnmbllem  23175  opnmblALT  23177  mbfimaicc  23206  ismbfd  23213  ismbf3d  23227  mbfimaopnlem  23228  mbfimaopn2  23230  i1fima  23251  i1fima2  23252  i1fd  23254  itg1addlem4  23272  ellimc2  23447  ellimc3  23449  dvres3  23483  dvres3a  23484  dvidlem  23485  dvcnp  23488  dvadd  23509  dvmul  23510  dvaddf  23511  dvmulf  23512  dvco  23516  dvcof  23517  dvcjbr  23518  dvcj  23519  dvrec  23524  dvcnvlem  23543  dvcnv  23544  dvef  23547  dvferm1  23552  dvferm2  23554  c1liplem1  23563  dvcnvrelem1  23584  dvcnvrelem2  23585  ftc1cn  23610  mdegcl  23633  deg1n0ima  23653  plyco0  23752  plyeq0  23771  plypf1  23772  plyaddlem1  23773  plymullem1  23774  tayl0  23920  ulmdvlem3  23960  ulmdv  23961  pserdv  23987  dvlog  24197  efopn  24204  relogbf  24329  dchrelbas2  24762  dchrghm  24781  uhgrfun  25732  uhgrafun  25829  eupap1  26503  sspg  26967  ssps  26969  sspn  26975  htthlem  27158  issh2  27450  hlimuni  27479  hhsscms  27520  occllem  27546  occl  27547  chscllem4  27883  imaelshi  28301  fmptcof2  28839  curry2ima  28869  fpwrelmapffslem  28895  xrofsup  28923  xrge0tsmsd  29116  smatrcl  29190  mdetpmtr1  29217  locfinreflem  29235  fsumcvg4  29324  zrhunitpreima  29350  esumpfinvallem  29463  imambfm  29651  carsggect  29707  sibfof  29729  sitgclg  29731  eulerpartlemd  29755  eulerpartlemt  29760  eulerpartlemmf  29764  eulerpartlemgvv  29765  eulerpartlemgu  29766  eulerpartlemgf  29768  dstrvprob  29860  dstfrvel  29862  orvclteinc  29864  erdszelem2  30428  erdszelem7  30433  erdszelem8  30434  cvmliftmolem1  30517  cvmliftlem3  30523  cvmliftlem10  30530  cvmliftlem13  30532  cvmliftlem15  30534  cvmlift2lem9  30547  cvmlift3lem6  30560  cvmlift3lem7  30561  mrsub0  30667  mrsubccat  30669  mrsubcn  30670  msubrn  30680  mclsax  30720  mthmblem  30731  mclsppslem  30734  mclspps  30735  nofun  31046  ivthALT  31500  icoreunrn  32383  icoreelrn  32385  curf  32557  curunc  32561  heicant  32614  opnmbllem0  32615  mblfinlem1  32616  itg2addnclem  32631  itg2addnclem2  32632  ftc1cnnc  32654  ftc1anclem7  32661  ftc1anc  32663  ftc2nc  32664  indexdom  32699  cnres2  32732  heibor1lem  32778  grpokerinj  32862  elrfirn  36276  fnwe2lem2  36639  lmhmfgima  36672  arearect  36820  areaquad  36821  funfvima2d  37491  cncmpmax  38214  fidmfisupp  38385  absfun  38507  evthiccabs  38565  ioofun  38625  limccog  38687  cncficcgt0  38774  dvsinax  38801  fperdvper  38808  fvvolioof  38882  fvvolicof  38884  dirkercncflem2  38997  fourierdlem20  39020  fourierdlem42  39042  fourierdlem63  39062  fourierdlem76  39075  fourierdlem82  39081  fourierdlem93  39092  fourierdlem97  39096  fourierdlem113  39112  fge0iccico  39263  sge0sn  39272  sge0tsms  39273  sge0cl  39274  sge0f1o  39275  sge0isum  39320  ovolval3  39537  ovnovollem1  39546  fmtnoinf  39986  pfxco  40301  subusgr  40513  vdegp1ai-av  40752  1wlkreslem  40878  pthdivtx  40935  pthdlem2lem  40973  elbigolo1  42149