Theorem ffun 6704

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6525  ⟶wf 6527

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 6534  df-f 6535

This theorem is used by:  ffund  6706  fco  6726  funssxp  6730  f00  6756  f1cof1  6782  fimadmfoALT  6799  dff3  7092  fliftf  7315  fiun  7944  f1iun  7945  fsuppeq  8176  fsuppeqg  8177  pmfun  8851  curf  8874  pmresg  8882  fodomr  9131  ac6sfi  9259  fodomfir  9303  fissuni  9330  fipreima  9331  ffsuppbi  9374  cnfcomlem  9684  tcrank  9882  fseqenlem2  10085  carduniima  10156  infmap2  10276  hsmexlem4  10488  hsmexlem5  10489  axdc3lem2  10510  axdc3lem4  10512  smobeth  10652  fpwwe2lem12  10708  inar1  10841  grur1  10886  nqerid  10999  fcdmnn0fsuppg  12647  zexALT  12694  hashkf  14456  hashgval  14457  revco  14965  ccatco  14966  pfxco  14969  lswco  14970  climdm  15701  isercolllem2  15813  isercolllem3  15814  isercoll  15815  sum0  15867  sumz  15868  fsumsers  15874  isumclim  15903  ntrivcvgfvn0  16048  ntrivcvgtail  16049  zprodn0  16086  iprodclim  16145  znnen  16360  isacs2  17807  isacs5  18702  dprdss  20225  dprd2dlem1  20237  dmdprdsplit2lem  20241  iscnp3  23542  subbascn  23552  cnpnei  23562  cnclima  23566  iscncl  23567  cncls  23572  cnrest2  23584  cnhaus  23652  kgencn3  23857  xkopt  23954  xkococnlem  23958  hmeores  24070  fbasrn  24183  uzrest  24196  rnelfmlem  24251  rnelfm  24252  fmfnfmlem3  24255  fmfnfmlem4  24256  fmfnfm  24257  cnflf2  24302  metcnp  24840  metustsym  24854  cfilucfil  24858  restmetu  24869  qtopbaslem  25057  tgqioo  25099  re2ndc  25100  bndth  25259  tcphcph  25538  ovolficcss  25770  volf  25830  volsup  25857  uniioombllem3a  25885  uniioombllem4  25887  uniioombllem5  25888  dyadmbllem  25900  dyadmbl  25901  opnmbllem  25902  opnmblALT  25904  mbfimaicc  25932  ismbf3d  25955  mbfimaopnlem  25956  mbfimaopn2  25958  i1fima  25979  i1fima2  25980  i1fd  25982  itg1addlem4  26000  dvidlem  26215  dvcnp  26219  dvadd  26240  dvmul  26241  dvaddf  26242  dvmulf  26243  dvco  26247  dvcof  26248  dvcjbr  26249  dvcj  26250  dvrec  26255  dvcnvlem  26276  dvef  26280  dvferm1  26285  dvferm2  26287  c1liplem1  26296  dvcnvrelem2  26318  mdegcl  26367  deg1n0ima  26387  plyco0  26490  plypf1  26511  tayl0  26671  ulmdvlem3  26711  pserdv  26738  dvlog  26961  efopn  26968  relogbf  27101  nofun  27988  madeval  28200  oldf  28205  oldlim  28255  madefi  28281  oldfi  28282  oldfib  28745  subusgr  29852  pthdivtx  30294  pthdlem2lem  30335  cyclnumvtx  30370  issh2  31793  hlimuni  31822  hhsscms  31862  occllem  31887  occl  31888  chscllem4  32224  imaelshi  32642  xrofsup  33341  tocyc01  33661  exsslsb  34211  dimval  34215  dimvalfi  34216  smatrcl  34410  mdetpmtr1  34437  locfinreflem  34454  fsumcvg4  34564  zrhunitpreima  34590  imambfm  34877  carsggect  34933  sibfof  34955  eulerpartlemt  34986  eulerpartlemmf  34990  eulerpartlemgvv  34991  eulerpartlemgf  34994  rpsqrtcn  35205  cardpred  35700  nummin  35701  erdszelem2  35926  erdszelem7  35931  erdszelem8  35932  cvmliftlem15  36032  mrsub0  36250  mrsubccat  36252  mrsubcn  36253  mthmblem  36314  ivthALT  37093  icoreunrn  38250  icoreelrn  38252  curunc  38493  heicant  38541  opnmbllem0  38542  mblfinlem1  38543  itg2addnclem  38557  itg2addnclem2  38558  ftc1anclem7  38585  ftc1anc  38587  ftc2nc  38588  indexdom  38636  cnres2  38665  aks6d1c6lem2  43189  elrfirn  43659  fnwe2lem2  44011  arearect  44175  areaquad  44176  naddcnff  44322  dfno2  44387  relpfr  45896  absfun  46306  evthiccabs  46452  ioofun  46507  cncficcgt0  46842  fperdvper  46873  fvvolioof  46943  fvvolicof  46945  fourierdlem20  47081  fourierdlem42  47103  fourierdlem63  47123  fourierdlem76  47136  fourierdlem93  47153  fourierdlem97  47157  ovolval3  47601  tannpoly  47884  sinnpoly  47885  uniimafveqt  48407  fundcmpsurbijinjpreimafv  48433  fundcmpsurbijinj  48436  fundcmpsurinjALT  48438  fmtnoinf  48565  isubgruhgr  48910  upgrimwlklem1  48939  elbigolo1  49613