Theorem ffun 6712

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6532  ⟶wf 6534

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 6541  df-f 6542

This theorem is used by:  ffund  6714  fco  6734  funssxp  6738  f00  6764  f1cof1  6790  fimadmfoALT  6807  dff3  7100  fliftf  7323  fiun  7955  f1iun  7956  fnwe2lem3  8149  fsuppeq  8195  fsuppeqg  8196  pmfun  8870  curf  8893  pmresg  8901  fodomr  9150  ac6sfi  9278  fodomfir  9322  fissuni  9349  fipreima  9350  ffsuppbi  9393  cnfcomlem  9703  tcrank  9904  fseqenlem2  10107  carduniima  10178  infmap2  10298  hsmexlem4  10510  hsmexlem5  10511  axdc3lem2  10532  axdc3lem4  10534  smobeth  10674  fpwwe2lem12  10730  inar1  10863  grur1  10908  nqerid  11021  fcdmnn0fsuppg  12669  zexALT  12716  hashkf  14479  hashgval  14480  revco  14989  ccatco  14990  pfxco  14993  lswco  14994  climdm  15726  isercolllem2  15838  isercolllem3  15839  isercoll  15840  sum0  15892  sumz  15893  fsumsers  15899  isumclim  15928  ntrivcvgfvn0  16073  ntrivcvgtail  16074  zprodn0  16111  iprodclim  16170  znnen  16385  isacs2  17832  isacs5  18727  dprdss  20250  dprd2dlem1  20262  dmdprdsplit2lem  20266  iscnp3  23567  subbascn  23577  cnpnei  23587  cnclima  23591  iscncl  23592  cncls  23597  cnrest2  23609  cnhaus  23677  kgencn3  23882  xkopt  23979  xkococnlem  23983  hmeores  24095  fbasrn  24208  uzrest  24221  rnelfmlem  24276  rnelfm  24277  fmfnfmlem3  24280  fmfnfmlem4  24281  fmfnfm  24282  cnflf2  24327  metcnp  24865  metustsym  24879  cfilucfil  24883  restmetu  24894  qtopbaslem  25082  tgqioo  25124  re2ndc  25125  bndth  25284  tcphcph  25563  ovolficcss  25795  volf  25855  volsup  25882  uniioombllem3a  25910  uniioombllem4  25912  uniioombllem5  25913  dyadmbllem  25925  dyadmbl  25926  opnmbllem  25927  opnmblALT  25929  mbfimaicc  25957  ismbf3d  25980  mbfimaopnlem  25981  mbfimaopn2  25983  i1fima  26004  i1fima2  26005  i1fd  26007  itg1addlem4  26025  dvidlem  26240  dvcnp  26244  dvadd  26265  dvmul  26266  dvaddf  26267  dvmulf  26268  dvco  26272  dvcof  26273  dvcjbr  26274  dvcj  26275  dvrec  26280  dvcnvlem  26301  dvef  26305  dvferm1  26310  dvferm2  26312  c1liplem1  26321  dvcnvrelem2  26343  mdegcl  26392  deg1n0ima  26412  plyco0  26515  plypf1  26536  tayl0  26694  ulmdvlem3  26734  pserdv  26761  dvlog  26984  efopn  26991  relogbf  27124  nofun  28011  madeval  28223  oldf  28228  oldlim  28278  madefi  28304  oldfi  28305  oldfib  28768  subusgr  29875  pthdivtx  30317  pthdlem2lem  30358  cyclnumvtx  30393  issh2  31816  hlimuni  31845  hhsscms  31885  occllem  31910  occl  31911  chscllem4  32247  imaelshi  32665  xrofsup  33405  tocyc01  33725  exsslsb  34275  dimval  34279  dimvalfi  34280  smatrcl  34474  mdetpmtr1  34501  locfinreflem  34518  fsumcvg4  34628  zrhunitpreima  34654  imambfm  34940  carsggect  34996  sibfof  35018  eulerpartlemt  35049  eulerpartlemmf  35053  eulerpartlemgvv  35054  eulerpartlemgf  35057  rpsqrtcn  35268  cardpred  35773  nummin  35774  acwer1prclem  35815  acwer1prc  35816  erdszelem2  36043  erdszelem7  36048  erdszelem8  36049  cvmliftlem15  36149  mrsub0  36367  mrsubccat  36369  mrsubcn  36370  mthmblem  36431  ivthALT  37215  icoreunrn  38375  icoreelrn  38377  curunc  38618  heicant  38666  opnmbllem0  38667  mblfinlem1  38668  itg2addnclem  38682  itg2addnclem2  38683  ftc1anclem7  38710  ftc1anc  38712  ftc2nc  38713  indexdom  38761  cnres2  38790  aks6d1c6lem2  43314  elrfirn  43799  arearect  44310  areaquad  44311  naddcnff  44457  dfno2  44522  relpfr  46037  absfun  46455  evthiccabs  46601  ioofun  46656  cncficcgt0  46991  fperdvper  47022  fvvolioof  47092  fvvolicof  47094  fourierdlem20  47230  fourierdlem42  47252  fourierdlem63  47272  fourierdlem76  47285  fourierdlem93  47302  fourierdlem97  47306  ovolval3  47750  tannpoly  48033  sinnpoly  48034  uniimafveqt  48556  fundcmpsurbijinjpreimafv  48582  fundcmpsurbijinj  48585  fundcmpsurinjALT  48587  fmtnoinf  48714  isubgruhgr  49059  upgrimwlklem1  49088  elbigolo1  49762