MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ffun Structured version   Visualization version   GIF version

Theorem ffun 6668
Description: A mapping is a function. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
ffun (𝐹:𝐴𝐵 → Fun 𝐹)

Proof of Theorem ffun
StepHypRef Expression
1 ffn 6665 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fnfun 6599 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝐹:𝐴𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6487   Fn wfn 6488  wf 6489
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 206  df-an 397  df-fn 6496  df-f 6497
This theorem is referenced by:  ffund  6669  fco  6689  funssxp  6694  f00  6721  f1cof1  6746  fimadmfoALT  6764  fimacnvOLD  7018  dff3  7046  fliftf  7256  fiun  7871  f1iun  7872  fsuppeq  8102  fsuppeqg  8103  pmfun  8781  pmresg  8804  fodomr  9068  ac6sfi  9227  fissuni  9297  fipreima  9298  ffsuppbi  9330  cnfcomlem  9631  tcrank  9816  fseqenlem2  9957  carduniima  10028  infmap2  10150  hsmexlem4  10361  hsmexlem5  10362  axdc3lem2  10383  axdc3lem4  10385  smobeth  10518  fpwwe2lem12  10574  inar1  10707  grur1  10752  nqerid  10865  fcdmnn0fsuppg  12468  zexALT  12515  hashkf  14224  hashgval  14225  revco  14715  ccatco  14716  pfxco  14719  lswco  14720  climdm  15428  isercolllem2  15542  isercolllem3  15543  isercoll  15544  sum0  15598  sumz  15599  fsumsers  15605  isumclim  15634  ntrivcvgfvn0  15776  ntrivcvgtail  15777  zprodn0  15814  iprodclim  15873  znnen  16086  isacs2  17525  isacs5  18429  dprdss  19799  dprd2dlem1  19811  dmdprdsplit2lem  19815  iscnp3  22579  subbascn  22589  cnpnei  22599  cnclima  22603  iscncl  22604  cncls  22609  cnrest2  22621  cnhaus  22689  kgencn3  22893  xkopt  22990  xkococnlem  22994  hmeores  23106  fbasrn  23219  uzrest  23232  rnelfmlem  23287  rnelfm  23288  fmfnfmlem3  23291  fmfnfmlem4  23292  fmfnfm  23293  cnflf2  23338  metcnp  23881  metustsym  23895  cfilucfil  23899  restmetu  23910  qtopbaslem  24106  tgqioo  24147  re2ndc  24148  bndth  24305  tcphcph  24585  ovolficcss  24817  volf  24877  volsup  24904  uniioombllem3a  24932  uniioombllem4  24934  uniioombllem5  24935  dyadmbllem  24947  dyadmbl  24948  opnmbllem  24949  opnmblALT  24951  mbfimaicc  24979  ismbf3d  25002  mbfimaopnlem  25003  mbfimaopn2  25005  i1fima  25026  i1fima2  25027  i1fd  25029  itg1addlem4  25047  itg1addlem4OLD  25048  dvidlem  25263  dvcnp  25267  dvadd  25288  dvmul  25289  dvaddf  25290  dvmulf  25291  dvco  25295  dvcof  25296  dvcjbr  25297  dvcj  25298  dvrec  25303  dvcnvlem  25324  dvef  25328  dvferm1  25333  dvferm2  25335  c1liplem1  25344  dvcnvrelem2  25366  mdegcl  25418  deg1n0ima  25438  plyco0  25537  plypf1  25557  tayl0  25705  ulmdvlem3  25745  pserdv  25772  dvlog  25990  efopn  25997  relogbf  26125  nofun  26981  madeval  27166  oldf  27171  oldlim  27200  subusgr  28123  pthdivtx  28563  pthdlem2lem  28601  issh2  30037  hlimuni  30066  hhsscms  30106  occllem  30131  occl  30132  chscllem4  30468  imaelshi  30886  xrofsup  31555  tocyc01  31850  dimval  32177  dimvalfi  32178  smatrcl  32246  mdetpmtr1  32273  locfinreflem  32290  fsumcvg4  32400  zrhunitpreima  32428  imambfm  32731  carsggect  32787  sibfof  32809  eulerpartlemt  32840  eulerpartlemmf  32844  eulerpartlemgvv  32845  eulerpartlemgf  32848  rpsqrtcn  33075  cardpred  33563  nummin  33564  erdszelem2  33655  erdszelem7  33660  erdszelem8  33661  cvmliftlem15  33761  mrsub0  33979  mrsubccat  33981  mrsubcn  33982  mthmblem  34043  ivthALT  34774  icoreunrn  35797  icoreelrn  35799  curf  36023  curunc  36027  heicant  36080  opnmbllem0  36081  mblfinlem1  36082  itg2addnclem  36096  itg2addnclem2  36097  ftc1anclem7  36124  ftc1anc  36126  ftc2nc  36127  indexdom  36160  cnres2  36189  elrfirn  40956  fnwe2lem2  41316  arearect  41487  areaquad  41488  naddcnff  41614  dfno2  41642  absfun  43520  evthiccabs  43666  ioofun  43721  cncficcgt0  44061  fperdvper  44092  fvvolioof  44162  fvvolicof  44164  fourierdlem20  44300  fourierdlem42  44322  fourierdlem63  44342  fourierdlem76  44355  fourierdlem93  44372  fourierdlem97  44376  fourierdlem113  44392  ovolval3  44820  uniimafveqt  45505  fundcmpsurbijinjpreimafv  45531  fundcmpsurbijinj  45534  fundcmpsurinjALT  45536  fmtnoinf  45660  elbigolo1  46575
  Copyright terms: Public domain W3C validator