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 𝐹)

Syntax hints:   → wi 4  Fun wfun 6531  ⟶wf 6533

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

This theorem is referenced by:  ffund  6711  fco  6731  funssxp  6735  f00  6761  f1cof1  6787  fimadmfoALT  6804  dff3  7096  fliftf  7314  fiun  7939  f1iun  7940  fsuppeq  8170  fsuppeqg  8171  pmfun  8843  pmresg  8867  fodomr  9115  ac6sfi  9243  fodomfir  9286  fissuni  9313  fipreima  9314  ffsuppbi  9357  cnfcomlem  9667  tcrank  9855  fseqenlem2  10008  carduniima  10079  infmap2  10199  hsmexlem4  10412  hsmexlem5  10413  axdc3lem2  10434  axdc3lem4  10436  smobeth  10570  fpwwe2lem12  10626  inar1  10759  grur1  10804  nqerid  10917  fcdmnn0fsuppg  12563  zexALT  12610  hashkf  14367  hashgval  14368  revco  14870  ccatco  14871  pfxco  14874  lswco  14875  climdm  15604  isercolllem2  15716  isercolllem3  15717  isercoll  15718  sum0  15771  sumz  15772  fsumsers  15778  isumclim  15807  ntrivcvgfvn0  15952  ntrivcvgtail  15953  zprodn0  15992  iprodclim  16051  znnen  16267  isacs2  17708  isacs5  18603  dprdss  20100  dprd2dlem1  20112  dmdprdsplit2lem  20116  iscnp3  23369  subbascn  23379  cnpnei  23389  cnclima  23393  iscncl  23394  cncls  23399  cnrest2  23411  cnhaus  23479  kgencn3  23683  xkopt  23780  xkococnlem  23784  hmeores  23896  fbasrn  24009  uzrest  24022  rnelfmlem  24077  rnelfm  24078  fmfnfmlem3  24081  fmfnfmlem4  24082  fmfnfm  24083  cnflf2  24128  metcnp  24666  metustsym  24680  cfilucfil  24684  restmetu  24695  qtopbaslem  24883  tgqioo  24925  re2ndc  24926  bndth  25085  tcphcph  25364  ovolficcss  25596  volf  25656  volsup  25683  uniioombllem3a  25711  uniioombllem4  25713  uniioombllem5  25714  dyadmbllem  25726  dyadmbl  25727  opnmbllem  25728  opnmblALT  25730  mbfimaicc  25758  ismbf3d  25781  mbfimaopnlem  25782  mbfimaopn2  25784  i1fima  25805  i1fima2  25806  i1fd  25808  itg1addlem4  25826  dvidlem  26042  dvcnp  26046  dvadd  26067  dvmul  26068  dvaddf  26069  dvmulf  26070  dvco  26074  dvcof  26075  dvcjbr  26076  dvcj  26077  dvrec  26082  dvcnvlem  26103  dvef  26107  dvferm1  26112  dvferm2  26114  c1liplem1  26123  dvcnvrelem2  26145  mdegcl  26194  deg1n0ima  26214  plyco0  26317  plypf1  26337  tayl0  26490  ulmdvlem3  26530  pserdv  26557  dvlog  26781  efopn  26788  relogbf  26921  nofun  27778  madeval  27990  oldf  27995  oldlim  28045  madefi  28071  oldfi  28072  oldfib  28535  subusgr  29579  pthdivtx  30016  pthdlem2lem  30056  cyclnumvtx  30089  issh2  31501  hlimuni  31530  hhsscms  31570  occllem  31595  occl  31596  chscllem4  31932  imaelshi  32350  xrofsup  33052  tocyc01  33378  exsslsb  33931  dimval  33935  dimvalfi  33936  smatrcl  34130  mdetpmtr1  34157  locfinreflem  34174  fsumcvg4  34284  zrhunitpreima  34310  imambfm  34596  carsggect  34652  sibfof  34674  eulerpartlemt  34705  eulerpartlemmf  34709  eulerpartlemgvv  34710  eulerpartlemgf  34713  rpsqrtcn  34924  cardpred  35425  nummin  35426  erdszelem2  35582  erdszelem7  35587  erdszelem8  35588  cvmliftlem15  35688  mrsub0  35906  mrsubccat  35908  mrsubcn  35909  mthmblem  35970  ivthALT  36734  icoreunrn  37892  icoreelrn  37894  curf  38136  curunc  38140  heicant  38193  opnmbllem0  38194  mblfinlem1  38195  itg2addnclem  38209  itg2addnclem2  38210  ftc1anclem7  38237  ftc1anc  38239  ftc2nc  38240  indexdom  38272  cnres2  38301  aks6d1c6lem2  42827  elrfirn  43317  fnwe2lem2  43669  arearect  43833  areaquad  43834  naddcnff  43980  dfno2  44045  relpfr  45554  absfun  45957  evthiccabs  46103  ioofun  46158  cncficcgt0  46493  fperdvper  46524  fvvolioof  46594  fvvolicof  46596  fourierdlem20  46732  fourierdlem42  46754  fourierdlem63  46774  fourierdlem76  46787  fourierdlem93  46804  fourierdlem97  46808  ovolval3  47252  tannpoly  47515  sinnpoly  47516  uniimafveqt  48018  fundcmpsurbijinjpreimafv  48044  fundcmpsurbijinj  48047  fundcmpsurinjALT  48049  fmtnoinf  48176  isubgruhgr  48521  upgrimwlklem1  48550  elbigolo1  49221