Theorem ffun 6715

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 6712	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2	1	fnfund 6643	1 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)

This proof depends on syntax axioms:   → wi 4  Fun wfun 6537  ⟶wf 6539

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 6546  df-f 6547

This theorem is used by:  ffund  6717  fco  6737  funssxp  6741  f00  6767  f1cof1  6793  fimadmfoALT  6810  dff3  7102  fliftf  7324  fiun  7949  f1iun  7950  fsuppeq  8180  fsuppeqg  8181  pmfun  8853  pmresg  8877  fodomr  9126  ac6sfi  9254  fodomfir  9297  fissuni  9324  fipreima  9325  ffsuppbi  9368  cnfcomlem  9678  tcrank  9866  fseqenlem2  10028  carduniima  10099  infmap2  10219  hsmexlem4  10431  hsmexlem5  10432  axdc3lem2  10453  axdc3lem4  10455  smobeth  10589  fpwwe2lem12  10645  inar1  10778  grur1  10823  nqerid  10936  fcdmnn0fsuppg  12582  zexALT  12629  hashkf  14388  hashgval  14389  revco  14897  ccatco  14898  pfxco  14901  lswco  14902  climdm  15631  isercolllem2  15743  isercolllem3  15744  isercoll  15745  sum0  15798  sumz  15799  fsumsers  15805  isumclim  15834  ntrivcvgfvn0  15979  ntrivcvgtail  15980  zprodn0  16019  iprodclim  16078  znnen  16293  isacs2  17734  isacs5  18629  dprdss  20132  dprd2dlem1  20144  dmdprdsplit2lem  20148  iscnp3  23438  subbascn  23448  cnpnei  23458  cnclima  23462  iscncl  23463  cncls  23468  cnrest2  23480  cnhaus  23548  kgencn3  23752  xkopt  23849  xkococnlem  23853  hmeores  23965  fbasrn  24078  uzrest  24091  rnelfmlem  24146  rnelfm  24147  fmfnfmlem3  24150  fmfnfmlem4  24151  fmfnfm  24152  cnflf2  24197  metcnp  24735  metustsym  24749  cfilucfil  24753  restmetu  24764  qtopbaslem  24952  tgqioo  24994  re2ndc  24995  bndth  25154  tcphcph  25433  ovolficcss  25665  volf  25725  volsup  25752  uniioombllem3a  25780  uniioombllem4  25782  uniioombllem5  25783  dyadmbllem  25795  dyadmbl  25796  opnmbllem  25797  opnmblALT  25799  mbfimaicc  25827  ismbf3d  25850  mbfimaopnlem  25851  mbfimaopn2  25853  i1fima  25874  i1fima2  25875  i1fd  25877  itg1addlem4  25895  dvidlem  26111  dvcnp  26115  dvadd  26136  dvmul  26137  dvaddf  26138  dvmulf  26139  dvco  26143  dvcof  26144  dvcjbr  26145  dvcj  26146  dvrec  26151  dvcnvlem  26172  dvef  26176  dvferm1  26181  dvferm2  26183  c1liplem1  26192  dvcnvrelem2  26214  mdegcl  26263  deg1n0ima  26283  plyco0  26386  plypf1  26406  tayl0  26562  ulmdvlem3  26602  pserdv  26629  dvlog  26853  efopn  26860  relogbf  26993  nofun  27850  madeval  28062  oldf  28067  oldlim  28117  madefi  28143  oldfi  28144  oldfib  28607  subusgr  29676  pthdivtx  30113  pthdlem2lem  30153  cyclnumvtx  30186  issh2  31598  hlimuni  31627  hhsscms  31667  occllem  31692  occl  31693  chscllem4  32029  imaelshi  32447  xrofsup  33149  tocyc01  33469  exsslsb  34018  dimval  34022  dimvalfi  34023  smatrcl  34217  mdetpmtr1  34244  locfinreflem  34261  fsumcvg4  34371  zrhunitpreima  34397  imambfm  34683  carsggect  34739  sibfof  34761  eulerpartlemt  34792  eulerpartlemmf  34796  eulerpartlemgvv  34797  eulerpartlemgf  34800  rpsqrtcn  35011  cardpred  35507  nummin  35508  erdszelem2  35704  erdszelem7  35709  erdszelem8  35710  cvmliftlem15  35810  mrsub0  36028  mrsubccat  36030  mrsubcn  36031  mthmblem  36092  ivthALT  36886  icoreunrn  38045  icoreelrn  38047  curf  38289  curunc  38293  heicant  38346  opnmbllem0  38347  mblfinlem1  38348  itg2addnclem  38362  itg2addnclem2  38363  ftc1anclem7  38390  ftc1anc  38392  ftc2nc  38393  indexdom  38425  cnres2  38454  aks6d1c6lem2  42978  elrfirn  43466  fnwe2lem2  43818  arearect  43982  areaquad  43983  naddcnff  44129  dfno2  44194  relpfr  45703  absfun  46106  evthiccabs  46252  ioofun  46307  cncficcgt0  46642  fperdvper  46673  fvvolioof  46743  fvvolicof  46745  fourierdlem20  46881  fourierdlem42  46903  fourierdlem63  46923  fourierdlem76  46936  fourierdlem93  46953  fourierdlem97  46957  ovolval3  47401  tannpoly  47667  sinnpoly  47668  uniimafveqt  48170  fundcmpsurbijinjpreimafv  48196  fundcmpsurbijinj  48199  fundcmpsurinjALT  48201  fmtnoinf  48328  isubgruhgr  48673  upgrimwlklem1  48702  elbigolo1  49377