Theorem ffun 6710

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

Syntax hints:   → wi 4  Fun wfun 6532  ⟶wf 6534

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

This theorem is referenced by:  ffund  6712  fco  6732  funssxp  6736  f00  6762  f1cof1  6788  fimadmfoALT  6805  dff3  7097  fliftf  7315  fiun  7941  f1iun  7942  fsuppeq  8172  fsuppeqg  8173  pmfun  8845  pmresg  8869  fodomr  9117  ac6sfi  9245  fodomfir  9288  fissuni  9315  fipreima  9316  ffsuppbi  9359  cnfcomlem  9669  tcrank  9857  fseqenlem2  10010  carduniima  10081  infmap2  10201  hsmexlem4  10414  hsmexlem5  10415  axdc3lem2  10436  axdc3lem4  10438  smobeth  10572  fpwwe2lem12  10628  inar1  10761  grur1  10806  nqerid  10919  fcdmnn0fsuppg  12565  zexALT  12612  hashkf  14370  hashgval  14371  revco  14873  ccatco  14874  pfxco  14877  lswco  14878  climdm  15607  isercolllem2  15719  isercolllem3  15720  isercoll  15721  sum0  15774  sumz  15775  fsumsers  15781  isumclim  15810  ntrivcvgfvn0  15955  ntrivcvgtail  15956  zprodn0  15995  iprodclim  16054  znnen  16269  isacs2  17710  isacs5  18605  dprdss  20102  dprd2dlem1  20114  dmdprdsplit2lem  20118  iscnp3  23382  subbascn  23392  cnpnei  23402  cnclima  23406  iscncl  23407  cncls  23412  cnrest2  23424  cnhaus  23492  kgencn3  23696  xkopt  23793  xkococnlem  23797  hmeores  23909  fbasrn  24022  uzrest  24035  rnelfmlem  24090  rnelfm  24091  fmfnfmlem3  24094  fmfnfmlem4  24095  fmfnfm  24096  cnflf2  24141  metcnp  24679  metustsym  24693  cfilucfil  24697  restmetu  24708  qtopbaslem  24896  tgqioo  24938  re2ndc  24939  bndth  25098  tcphcph  25377  ovolficcss  25609  volf  25669  volsup  25696  uniioombllem3a  25724  uniioombllem4  25726  uniioombllem5  25727  dyadmbllem  25739  dyadmbl  25740  opnmbllem  25741  opnmblALT  25743  mbfimaicc  25771  ismbf3d  25794  mbfimaopnlem  25795  mbfimaopn2  25797  i1fima  25818  i1fima2  25819  i1fd  25821  itg1addlem4  25839  dvidlem  26055  dvcnp  26059  dvadd  26080  dvmul  26081  dvaddf  26082  dvmulf  26083  dvco  26087  dvcof  26088  dvcjbr  26089  dvcj  26090  dvrec  26095  dvcnvlem  26116  dvef  26120  dvferm1  26125  dvferm2  26127  c1liplem1  26136  dvcnvrelem2  26158  mdegcl  26207  deg1n0ima  26227  plyco0  26330  plypf1  26350  tayl0  26503  ulmdvlem3  26543  pserdv  26570  dvlog  26794  efopn  26801  relogbf  26934  nofun  27791  madeval  28003  oldf  28008  oldlim  28058  madefi  28084  oldfi  28085  oldfib  28548  subusgr  29617  pthdivtx  30054  pthdlem2lem  30094  cyclnumvtx  30127  issh2  31539  hlimuni  31568  hhsscms  31608  occllem  31633  occl  31634  chscllem4  31970  imaelshi  32388  xrofsup  33090  tocyc01  33416  exsslsb  33965  dimval  33969  dimvalfi  33970  smatrcl  34164  mdetpmtr1  34191  locfinreflem  34208  fsumcvg4  34318  zrhunitpreima  34344  imambfm  34630  carsggect  34686  sibfof  34708  eulerpartlemt  34739  eulerpartlemmf  34743  eulerpartlemgvv  34744  eulerpartlemgf  34747  rpsqrtcn  34958  cardpred  35461  nummin  35462  erdszelem2  35662  erdszelem7  35667  erdszelem8  35668  cvmliftlem15  35768  mrsub0  35986  mrsubccat  35988  mrsubcn  35989  mthmblem  36050  ivthALT  36824  icoreunrn  37983  icoreelrn  37985  curf  38227  curunc  38231  heicant  38284  opnmbllem0  38285  mblfinlem1  38286  itg2addnclem  38300  itg2addnclem2  38301  ftc1anclem7  38328  ftc1anc  38330  ftc2nc  38331  indexdom  38363  cnres2  38392  aks6d1c6lem2  42916  elrfirn  43406  fnwe2lem2  43758  arearect  43922  areaquad  43923  naddcnff  44069  dfno2  44134  relpfr  45643  absfun  46046  evthiccabs  46192  ioofun  46247  cncficcgt0  46582  fperdvper  46613  fvvolioof  46683  fvvolicof  46685  fourierdlem20  46821  fourierdlem42  46843  fourierdlem63  46863  fourierdlem76  46876  fourierdlem93  46893  fourierdlem97  46897  ovolval3  47341  tannpoly  47604  sinnpoly  47605  uniimafveqt  48107  fundcmpsurbijinjpreimafv  48133  fundcmpsurbijinj  48136  fundcmpsurinjALT  48138  fmtnoinf  48265  isubgruhgr  48610  upgrimwlklem1  48639  elbigolo1  49314