Theorem ffun 6709

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6531  ⟶wf 6533

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

This theorem is used by:  ffund  6711  fco  6731  funssxp  6735  f00  6761  f1cof1  6787  fimadmfoALT  6804  dff3  7097  fliftf  7320  fiun  7944  f1iun  7945  fsuppeq  8177  fsuppeqg  8178  pmfun  8850  curf  8873  pmresg  8881  fodomr  9130  ac6sfi  9258  fodomfir  9301  fissuni  9328  fipreima  9329  ffsuppbi  9372  cnfcomlem  9682  tcrank  9870  fseqenlem2  10032  carduniima  10103  infmap2  10223  hsmexlem4  10435  hsmexlem5  10436  axdc3lem2  10457  axdc3lem4  10459  smobeth  10599  fpwwe2lem12  10655  inar1  10788  grur1  10833  nqerid  10946  fcdmnn0fsuppg  12592  zexALT  12639  hashkf  14400  hashgval  14401  revco  14909  ccatco  14910  pfxco  14913  lswco  14914  climdm  15645  isercolllem2  15757  isercolllem3  15758  isercoll  15759  sum0  15811  sumz  15812  fsumsers  15818  isumclim  15847  ntrivcvgfvn0  15992  ntrivcvgtail  15993  zprodn0  16032  iprodclim  16091  znnen  16306  isacs2  17747  isacs5  18642  dprdss  20164  dprd2dlem1  20176  dmdprdsplit2lem  20180  iscnp3  23475  subbascn  23485  cnpnei  23495  cnclima  23499  iscncl  23500  cncls  23505  cnrest2  23517  cnhaus  23585  kgencn3  23790  xkopt  23887  xkococnlem  23891  hmeores  24003  fbasrn  24116  uzrest  24129  rnelfmlem  24184  rnelfm  24185  fmfnfmlem3  24188  fmfnfmlem4  24189  fmfnfm  24190  cnflf2  24235  metcnp  24773  metustsym  24787  cfilucfil  24791  restmetu  24802  qtopbaslem  24990  tgqioo  25032  re2ndc  25033  bndth  25192  tcphcph  25471  ovolficcss  25703  volf  25763  volsup  25790  uniioombllem3a  25818  uniioombllem4  25820  uniioombllem5  25821  dyadmbllem  25833  dyadmbl  25834  opnmbllem  25835  opnmblALT  25837  mbfimaicc  25865  ismbf3d  25888  mbfimaopnlem  25889  mbfimaopn2  25891  i1fima  25912  i1fima2  25913  i1fd  25915  itg1addlem4  25933  dvidlem  26149  dvcnp  26153  dvadd  26174  dvmul  26175  dvaddf  26176  dvmulf  26177  dvco  26181  dvcof  26182  dvcjbr  26183  dvcj  26184  dvrec  26189  dvcnvlem  26210  dvef  26214  dvferm1  26219  dvferm2  26221  c1liplem1  26230  dvcnvrelem2  26252  mdegcl  26301  deg1n0ima  26321  plyco0  26424  plypf1  26445  tayl0  26605  ulmdvlem3  26645  pserdv  26672  dvlog  26896  efopn  26903  relogbf  27036  nofun  27893  madeval  28105  oldf  28110  oldlim  28160  madefi  28186  oldfi  28187  oldfib  28650  subusgr  29757  pthdivtx  30199  pthdlem2lem  30240  cyclnumvtx  30275  issh2  31698  hlimuni  31727  hhsscms  31767  occllem  31792  occl  31793  chscllem4  32129  imaelshi  32547  xrofsup  33246  tocyc01  33566  exsslsb  34115  dimval  34119  dimvalfi  34120  smatrcl  34314  mdetpmtr1  34341  locfinreflem  34358  fsumcvg4  34468  zrhunitpreima  34494  imambfm  34781  carsggect  34837  sibfof  34859  eulerpartlemt  34890  eulerpartlemmf  34894  eulerpartlemgvv  34895  eulerpartlemgf  34898  rpsqrtcn  35109  cardpred  35605  nummin  35606  erdszelem2  35779  erdszelem7  35784  erdszelem8  35785  cvmliftlem15  35885  mrsub0  36103  mrsubccat  36105  mrsubcn  36106  mthmblem  36167  ivthALT  36962  icoreunrn  38121  icoreelrn  38123  curunc  38364  heicant  38412  opnmbllem0  38413  mblfinlem1  38414  itg2addnclem  38428  itg2addnclem2  38429  ftc1anclem7  38456  ftc1anc  38458  ftc2nc  38459  indexdom  38492  cnres2  38521  aks6d1c6lem2  43045  elrfirn  43548  fnwe2lem2  43900  arearect  44064  areaquad  44065  naddcnff  44211  dfno2  44276  relpfr  45785  absfun  46188  evthiccabs  46334  ioofun  46389  cncficcgt0  46724  fperdvper  46755  fvvolioof  46825  fvvolicof  46827  fourierdlem20  46963  fourierdlem42  46985  fourierdlem63  47005  fourierdlem76  47018  fourierdlem93  47035  fourierdlem97  47039  ovolval3  47483  tannpoly  47766  sinnpoly  47767  uniimafveqt  48289  fundcmpsurbijinjpreimafv  48315  fundcmpsurbijinj  48318  fundcmpsurinjALT  48320  fmtnoinf  48447  isubgruhgr  48792  upgrimwlklem1  48821  elbigolo1  49495