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

Theorem ffun 6516
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 6513 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fnfun 6452 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝐹:𝐴𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6348   Fn wfn 6349  wf 6350
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 208  df-an 397  df-fn 6357  df-f 6358
This theorem is referenced by:  ffund  6517  funssxp  6534  f00  6560  fimadmfoALT  6600  fimacnv  6837  dff3  6864  fliftf  7062  fiunw  7637  f1iunw  7638  fiun  7640  f1iun  7641  frnsuppeq  7838  pmfun  8421  pmresg  8429  fodomr  8662  ac6sfi  8756  fissuni  8823  fipreima  8824  frnfsuppbi  8856  cnfcomlem  9156  tcrank  9307  fseqenlem2  9445  carduniima  9516  infmap2  9634  hsmexlem4  9845  hsmexlem5  9846  axdc3lem2  9867  axdc3lem4  9869  smobeth  10002  fpwwe2lem13  10058  inar1  10191  grur1  10236  nqerid  10349  zexALT  11995  hashkf  13687  hashgval  13688  revco  14191  ccatco  14192  pfxco  14195  lswco  14196  climdm  14906  isercolllem2  15017  isercolllem3  15018  isercoll  15019  sum0  15073  sumz  15074  fsumsers  15080  isumclim  15107  ntrivcvgfvn0  15250  ntrivcvgtail  15251  zprodn0  15288  iprodclim  15347  znnen  15560  isacs2  16919  isacs5  17777  dprdss  19087  dprd2dlem1  19099  dmdprdsplit2lem  19103  iscnp3  21787  subbascn  21797  cnpnei  21807  cnclima  21811  iscncl  21812  cncls  21817  cnrest2  21829  cnhaus  21897  kgencn3  22101  xkopt  22198  xkococnlem  22202  hmeores  22314  fbasrn  22427  uzrest  22440  rnelfmlem  22495  rnelfm  22496  fmfnfmlem3  22499  fmfnfmlem4  22500  fmfnfm  22501  cnflf2  22546  metcnp  23085  metustsym  23099  cfilucfil  23103  restmetu  23114  qtopbaslem  23301  tgqioo  23342  re2ndc  23343  bndth  23496  tcphcph  23774  ovolficcss  24004  volf  24064  volsup  24091  uniioombllem3a  24119  uniioombllem4  24121  uniioombllem5  24122  dyadmbllem  24134  dyadmbl  24135  opnmbllem  24136  opnmblALT  24138  mbfimaicc  24166  ismbf3d  24189  mbfimaopnlem  24190  mbfimaopn2  24192  i1fima  24213  i1fima2  24214  i1fd  24216  itg1addlem4  24234  dvidlem  24447  dvcnp  24450  dvadd  24471  dvmul  24472  dvaddf  24473  dvmulf  24474  dvco  24478  dvcof  24479  dvcjbr  24480  dvcj  24481  dvrec  24486  dvcnvlem  24507  dvef  24511  dvferm1  24516  dvferm2  24518  c1liplem1  24527  dvcnvrelem2  24549  mdegcl  24597  deg1n0ima  24617  plyco0  24716  plypf1  24736  tayl0  24884  ulmdvlem3  24924  pserdv  24951  dvlog  25166  efopn  25173  relogbf  25301  subusgr  27004  pthdivtx  27443  pthdlem2lem  27481  issh2  28919  hlimuni  28948  hhsscms  28988  occllem  29013  occl  29014  chscllem4  29350  imaelshi  29768  xrofsup  30424  tocyc01  30693  dimval  30906  dimvalfi  30907  smatrcl  30966  mdetpmtr1  30993  locfinreflem  31009  fsumcvg4  31098  zrhunitpreima  31124  imambfm  31425  carsggect  31481  sibfof  31503  eulerpartlemt  31534  eulerpartlemmf  31538  eulerpartlemgvv  31539  eulerpartlemgf  31542  rpsqrtcn  31769  erdszelem2  32342  erdszelem7  32347  erdszelem8  32348  cvmliftlem15  32448  mrsub0  32666  mrsubccat  32668  mrsubcn  32669  mthmblem  32730  nofun  33059  madeval  33192  ivthALT  33586  icoreunrn  34528  icoreelrn  34530  curf  34756  curunc  34760  heicant  34813  opnmbllem0  34814  mblfinlem1  34815  itg2addnclem  34829  itg2addnclem2  34830  ftc1anclem7  34859  ftc1anc  34861  ftc2nc  34862  indexdom  34896  cnres2  34928  elrfirn  39176  fnwe2lem2  39535  arearect  39706  areaquad  39707  absfun  41502  evthiccabs  41655  ioofun  41711  cncficcgt0  42055  fperdvper  42087  fvvolioof  42159  fvvolicof  42161  fourierdlem20  42297  fourierdlem42  42319  fourierdlem63  42339  fourierdlem76  42352  fourierdlem93  42369  fourierdlem97  42373  fourierdlem113  42389  ovolval3  42814  fmtnoinf  43549  elbigolo1  44519
  Copyright terms: Public domain W3C validator