Theorem ffun 6734

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6552  ⟶wf 6554

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 6561  df-f 6562

This theorem is used by:  ffund  6736  fco  6756  funssxp  6760  f00  6786  f1cof1  6812  fimadmfoALT  6829  dff3  7124  fliftf  7346  fiun  7979  f1iun  7980  fnwe2lem3  8174  fsuppeq  8220  fsuppeqg  8221  pmfun  8895  curf  8918  pmresg  8926  fodomr  9175  ac6sfi  9303  fodomfir  9347  fissuni  9374  fipreima  9375  ffsuppbi  9417  cnfcomlem  9727  tcrank  9928  fseqenlem2  10131  carduniima  10202  infmap2  10322  hsmexlem4  10534  hsmexlem5  10535  axdc3lem2  10556  axdc3lem4  10558  smobeth  10698  fpwwe2lem12  10754  inar1  10887  grur1  10932  nqerid  11045  fcdmnn0fsuppg  12693  zexALT  12740  hashkf  14503  hashgval  14504  revco  15013  ccatco  15014  pfxco  15017  lswco  15018  climdm  15750  isercolllem2  15862  isercolllem3  15863  isercoll  15864  sum0  15916  sumz  15917  fsumsers  15923  isumclim  15952  ntrivcvgfvn0  16097  ntrivcvgtail  16098  zprodn0  16135  iprodclim  16194  znnen  16409  isacs2  17856  isacs5  18751  dprdss  20275  dprd2dlem1  20287  dmdprdsplit2lem  20291  iscnp3  23592  subbascn  23602  cnpnei  23612  cnclima  23616  iscncl  23617  cncls  23622  cnrest2  23634  cnhaus  23702  kgencn3  23907  xkopt  24004  xkococnlem  24008  hmeores  24120  fbasrn  24233  uzrest  24246  rnelfmlem  24301  rnelfm  24302  fmfnfmlem3  24305  fmfnfmlem4  24306  fmfnfm  24307  cnflf2  24352  metcnp  24890  metustsym  24904  cfilucfil  24908  restmetu  24919  qtopbaslem  25107  tgqioo  25149  re2ndc  25150  bndth  25309  tcphcph  25588  ovolficcss  25820  volf  25880  volsup  25907  uniioombllem3a  25935  uniioombllem4  25937  uniioombllem5  25938  dyadmbllem  25950  dyadmbl  25951  opnmbllem  25952  opnmblALT  25954  mbfimaicc  25982  ismbf3d  26005  mbfimaopnlem  26006  mbfimaopn2  26008  i1fima  26029  i1fima2  26030  i1fd  26032  itg1addlem4  26050  dvidlem  26265  dvcnp  26269  dvadd  26290  dvmul  26291  dvaddf  26292  dvmulf  26293  dvco  26297  dvcof  26298  dvcjbr  26299  dvcj  26300  dvrec  26305  dvcnvlem  26326  dvef  26330  dvferm1  26335  dvferm2  26337  c1liplem1  26346  dvcnvrelem2  26368  mdegcl  26417  deg1n0ima  26437  plyco0  26540  plypf1  26561  tayl0  26719  ulmdvlem3  26759  pserdv  26786  dvlog  27009  efopn  27016  relogbf  27149  nofun  28036  madeval  28248  oldf  28253  oldlim  28303  madefi  28329  oldfi  28330  oldfib  28793  subusgr  29900  pthdivtx  30342  pthdlem2lem  30383  cyclnumvtx  30418  issh2  31841  hlimuni  31870  hhsscms  31910  occllem  31935  occl  31936  chscllem4  32272  imaelshi  32690  xrofsup  33429  tocyc01  33749  exsslsb  34299  dimval  34303  dimvalfi  34304  smatrcl  34498  mdetpmtr1  34525  locfinreflem  34542  fsumcvg4  34652  zrhunitpreima  34678  imambfm  34964  carsggect  35020  sibfof  35042  eulerpartlemt  35073  eulerpartlemmf  35077  eulerpartlemgvv  35078  eulerpartlemgf  35081  rpsqrtcn  35292  cardpred  35805  nummin  35806  acwer1prclem  35851  acwer1prc  35852  erdszelem2  36124  erdszelem7  36129  erdszelem8  36130  cvmliftlem15  36230  mrsub0  36448  mrsubccat  36450  mrsubcn  36451  mthmblem  36512  ivthALT  37301  icoreunrn  38474  icoreelrn  38476  curunc  38717  heicant  38765  opnmbllem0  38766  mblfinlem1  38767  itg2addnclem  38781  itg2addnclem2  38782  ftc1anclem7  38809  ftc1anc  38811  ftc2nc  38812  indexdom  38860  cnres2  38889  aks6d1c6lem2  43413  elrfirn  43899  arearect  44409  areaquad  44410  naddcnff  44556  dfno2  44621  relpfr  46139  absfun  46567  evthiccabs  46713  ioofun  46768  cncficcgt0  47103  fperdvper  47134  fvvolioof  47204  fvvolicof  47206  fourierdlem20  47342  fourierdlem42  47364  fourierdlem63  47384  fourierdlem76  47397  fourierdlem93  47414  fourierdlem97  47418  ovolval3  47862  tannpoly  48145  sinnpoly  48146  uniimafveqt  48668  fundcmpsurbijinjpreimafv  48694  fundcmpsurbijinj  48697  fundcmpsurinjALT  48699  fmtnoinf  48826  isubgruhgr  49171  upgrimwlklem1  49200  elbigolo1  49874