Theorem ffun 6698

Description: A mapping is a function. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)

Assertion

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

Proof of Theorem ffun

Step	Hyp	Ref	Expression
1		ffn 6695	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2	1	fnfund 6626	1 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 6519  ⟶wf 6521

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 210  df-an 401  df-fn 6528  df-f 6529

This theorem is referenced by:  ffund  6700  fco  6720  funssxp  6724  f00  6750  f1cof1  6776  fimadmfoALT  6793  dff3  7085  fliftf  7303  fiun  7928  f1iun  7929  fsuppeq  8159  fsuppeqg  8160  pmfun  8832  pmresg  8856  fodomr  9104  ac6sfi  9232  fodomfir  9275  fissuni  9302  fipreima  9303  ffsuppbi  9346  cnfcomlem  9656  tcrank  9844  fseqenlem2  9997  carduniima  10068  infmap2  10188  hsmexlem4  10401  hsmexlem5  10402  axdc3lem2  10423  axdc3lem4  10425  smobeth  10559  fpwwe2lem12  10615  inar1  10748  grur1  10793  nqerid  10906  fcdmnn0fsuppg  12555  zexALT  12602  hashkf  14359  hashgval  14360  revco  14861  ccatco  14862  pfxco  14865  lswco  14866  climdm  15595  isercolllem2  15707  isercolllem3  15708  isercoll  15709  sum0  15762  sumz  15763  fsumsers  15769  isumclim  15798  ntrivcvgfvn0  15943  ntrivcvgtail  15944  zprodn0  15983  iprodclim  16042  znnen  16258  isacs2  17699  isacs5  18594  dprdss  20092  dprd2dlem1  20104  dmdprdsplit2lem  20108  iscnp3  23362  subbascn  23372  cnpnei  23382  cnclima  23386  iscncl  23387  cncls  23392  cnrest2  23404  cnhaus  23472  kgencn3  23676  xkopt  23773  xkococnlem  23777  hmeores  23889  fbasrn  24002  uzrest  24015  rnelfmlem  24070  rnelfm  24071  fmfnfmlem3  24074  fmfnfmlem4  24075  fmfnfm  24076  cnflf2  24121  metcnp  24659  metustsym  24673  cfilucfil  24677  restmetu  24688  qtopbaslem  24876  tgqioo  24918  re2ndc  24919  bndth  25078  tcphcph  25357  ovolficcss  25589  volf  25649  volsup  25676  uniioombllem3a  25704  uniioombllem4  25706  uniioombllem5  25707  dyadmbllem  25719  dyadmbl  25720  opnmbllem  25721  opnmblALT  25723  mbfimaicc  25751  ismbf3d  25774  mbfimaopnlem  25775  mbfimaopn2  25777  i1fima  25798  i1fima2  25799  i1fd  25801  itg1addlem4  25819  dvidlem  26035  dvcnp  26039  dvadd  26060  dvmul  26061  dvaddf  26062  dvmulf  26063  dvco  26067  dvcof  26068  dvcjbr  26069  dvcj  26070  dvrec  26075  dvcnvlem  26096  dvef  26100  dvferm1  26105  dvferm2  26107  c1liplem1  26116  dvcnvrelem2  26138  mdegcl  26187  deg1n0ima  26207  plyco0  26310  plypf1  26330  tayl0  26483  ulmdvlem3  26523  pserdv  26550  dvlog  26774  efopn  26781  relogbf  26914  nofun  27771  madeval  27983  oldf  27988  oldlim  28038  madefi  28064  oldfi  28065  oldfib  28528  subusgr  29548  pthdivtx  29985  pthdlem2lem  30025  cyclnumvtx  30058  issh2  31470  hlimuni  31499  hhsscms  31539  occllem  31564  occl  31565  chscllem4  31901  imaelshi  32319  xrofsup  33024  tocyc01  33351  exsslsb  33904  dimval  33908  dimvalfi  33909  smatrcl  34103  mdetpmtr1  34130  locfinreflem  34147  fsumcvg4  34257  zrhunitpreima  34283  imambfm  34569  carsggect  34625  sibfof  34647  eulerpartlemt  34678  eulerpartlemmf  34682  eulerpartlemgvv  34683  eulerpartlemgf  34686  rpsqrtcn  34897  cardpred  35398  nummin  35399  erdszelem2  35555  erdszelem7  35560  erdszelem8  35561  cvmliftlem15  35661  mrsub0  35879  mrsubccat  35881  mrsubcn  35882  mthmblem  35943  ivthALT  36708  icoreunrn  37865  icoreelrn  37867  curf  38109  curunc  38113  heicant  38166  opnmbllem0  38167  mblfinlem1  38168  itg2addnclem  38182  itg2addnclem2  38183  ftc1anclem7  38210  ftc1anc  38212  ftc2nc  38213  indexdom  38245  cnres2  38274  aks6d1c6lem2  42800  elrfirn  43288  fnwe2lem2  43640  arearect  43804  areaquad  43805  naddcnff  43951  dfno2  44016  relpfr  45528  absfun  45924  evthiccabs  46070  ioofun  46125  cncficcgt0  46460  fperdvper  46491  fvvolioof  46561  fvvolicof  46563  fourierdlem20  46699  fourierdlem42  46721  fourierdlem63  46741  fourierdlem76  46754  fourierdlem93  46771  fourierdlem97  46775  ovolval3  47219  tannpoly  47482  sinnpoly  47483  uniimafveqt  47985  fundcmpsurbijinjpreimafv  48011  fundcmpsurbijinj  48014  fundcmpsurinjALT  48016  fmtnoinf  48143  isubgruhgr  48488  upgrimwlklem1  48517  elbigolo1  49188