Theorem ffun 6690

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

Syntax hints:   → wi 4  Fun wfun 6511  ⟶wf 6513

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 209  df-an 400  df-fn 6520  df-f 6521

This theorem is referenced by:  ffund  6692  fco  6712  funssxp  6716  f00  6742  f1cof1  6768  fimadmfoALT  6785  dff3  7077  fliftf  7295  fiun  7920  f1iun  7921  fsuppeq  8150  fsuppeqg  8151  pmfun  8824  pmresg  8848  fodomr  9096  ac6sfi  9224  fodomfir  9268  fissuni  9297  fipreima  9298  ffsuppbi  9341  cnfcomlem  9651  tcrank  9839  fseqenlem2  9978  carduniima  10049  infmap2  10170  hsmexlem4  10383  hsmexlem5  10384  axdc3lem2  10405  axdc3lem4  10407  smobeth  10541  fpwwe2lem12  10597  inar1  10730  grur1  10775  nqerid  10888  fcdmnn0fsuppg  12538  zexALT  12585  hashkf  14342  hashgval  14343  revco  14844  ccatco  14845  pfxco  14848  lswco  14849  climdm  15564  isercolllem2  15676  isercolllem3  15677  isercoll  15678  sum0  15731  sumz  15732  fsumsers  15738  isumclim  15767  ntrivcvgfvn0  15912  ntrivcvgtail  15913  zprodn0  15952  iprodclim  16011  znnen  16227  isacs2  17668  isacs5  18563  dprdss  20054  dprd2dlem1  20066  dmdprdsplit2lem  20070  iscnp3  23284  subbascn  23294  cnpnei  23304  cnclima  23308  iscncl  23309  cncls  23314  cnrest2  23326  cnhaus  23394  kgencn3  23598  xkopt  23695  xkococnlem  23699  hmeores  23811  fbasrn  23924  uzrest  23937  rnelfmlem  23992  rnelfm  23993  fmfnfmlem3  23996  fmfnfmlem4  23997  fmfnfm  23998  cnflf2  24043  metcnp  24581  metustsym  24595  cfilucfil  24599  restmetu  24610  qtopbaslem  24798  tgqioo  24840  re2ndc  24841  bndth  25000  tcphcph  25279  ovolficcss  25511  volf  25571  volsup  25598  uniioombllem3a  25626  uniioombllem4  25628  uniioombllem5  25629  dyadmbllem  25641  dyadmbl  25642  opnmbllem  25643  opnmblALT  25645  mbfimaicc  25673  ismbf3d  25696  mbfimaopnlem  25697  mbfimaopn2  25699  i1fima  25720  i1fima2  25721  i1fd  25723  itg1addlem4  25741  dvidlem  25957  dvcnp  25961  dvadd  25982  dvmul  25983  dvaddf  25984  dvmulf  25985  dvco  25989  dvcof  25990  dvcjbr  25991  dvcj  25992  dvrec  25997  dvcnvlem  26018  dvef  26022  dvferm1  26027  dvferm2  26029  c1liplem1  26038  dvcnvrelem2  26060  mdegcl  26109  deg1n0ima  26129  plyco0  26232  plypf1  26252  tayl0  26402  ulmdvlem3  26442  pserdv  26469  dvlog  26693  efopn  26700  relogbf  26833  nofun  27690  madeval  27902  oldf  27907  oldlim  27957  madefi  27983  oldfi  27984  oldfib  28447  subusgr  29436  pthdivtx  29873  pthdlem2lem  29913  cyclnumvtx  29946  issh2  31358  hlimuni  31387  hhsscms  31427  occllem  31452  occl  31453  chscllem4  31789  imaelshi  32207  xrofsup  32919  tocyc01  33259  exsslsb  33855  dimval  33859  dimvalfi  33860  smatrcl  34054  mdetpmtr1  34081  locfinreflem  34098  fsumcvg4  34208  zrhunitpreima  34234  imambfm  34520  carsggect  34576  sibfof  34598  eulerpartlemt  34629  eulerpartlemmf  34633  eulerpartlemgvv  34634  eulerpartlemgf  34637  rpsqrtcn  34851  cardpred  35352  nummin  35353  erdszelem2  35506  erdszelem7  35511  erdszelem8  35512  cvmliftlem15  35612  mrsub0  35830  mrsubccat  35832  mrsubcn  35833  mthmblem  35894  ivthALT  36659  icoreunrn  37817  icoreelrn  37819  curf  38061  curunc  38065  heicant  38118  opnmbllem0  38119  mblfinlem1  38120  itg2addnclem  38134  itg2addnclem2  38135  ftc1anclem7  38162  ftc1anc  38164  ftc2nc  38165  indexdom  38197  cnres2  38226  aks6d1c6lem2  42752  elrfirn  43240  fnwe2lem2  43592  arearect  43756  areaquad  43757  naddcnff  43903  dfno2  43968  relpfr  45494  absfun  45890  evthiccabs  46036  ioofun  46091  cncficcgt0  46426  fperdvper  46457  fvvolioof  46527  fvvolicof  46529  fourierdlem20  46665  fourierdlem42  46687  fourierdlem63  46707  fourierdlem76  46720  fourierdlem93  46737  fourierdlem97  46741  ovolval3  47185  tannpoly  47448  sinnpoly  47449  uniimafveqt  47951  fundcmpsurbijinjpreimafv  47977  fundcmpsurbijinj  47980  fundcmpsurinjALT  47982  fmtnoinf  48109  isubgruhgr  48454  upgrimwlklem1  48483  elbigolo1  49143