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

Theorem ffun 5738
Description: A mapping is a function. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
ffun

Proof of Theorem ffun
StepHypRef Expression
1 ffn 5736 . 2
2 fnfun 5683 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  Funwfun 5587  Fnwfn 5588  -->wf 5589
This theorem is referenced by:  funssxp  5749  f00  5772  fofun  5801  fimacnv  6019  dff3  6044  fmptco  6064  fliftf  6213  fun11iun  6760  frnsuppeq  6930  smores2  7044  pmfun  7458  elmapfun  7462  pmresg  7466  fodomr  7688  ac6sfi  7784  fissuni  7845  fipreima  7846  fdmfifsupp  7859  frnfsuppbi  7878  fsuppmptif  7879  fsuppco2  7882  fsuppcor  7883  ordtypelem8  7971  ordtypelem9  7972  ordtypelem10  7973  unxpwdom2  8035  cantnffvalOLD  8103  cnfcomlem  8164  cnfcomlemOLD  8172  tcrank  8323  fseqenlem2  8427  carduniima  8498  infmap2  8619  hsmexlem4  8830  hsmexlem5  8831  axdc3lem2  8852  axdc3lem4  8854  smobeth  8982  fpwwe2lem13  9041  fpwwe2  9042  inar1  9174  grur1  9219  nqerid  9332  nn0suppOLD  10875  zexALT  10908  hashkf  12407  hashgval  12408  hashfzdm  12498  hashfirdm  12500  revco  12800  ccatco  12801  lswco  12804  climdm  13377  isercolllem2  13488  isercolllem3  13489  isercoll  13490  sum0  13543  sumz  13544  fsumsers  13550  isumclim  13572  ntrivcvgfvn0  13708  ntrivcvgtail  13709  zprodn0  13746  iprodclim  13791  znnen  13946  mrcuni  15018  isacs2  15050  isacs5  15802  cntzmhm2  16377  frgpupval  16792  gsumzadd  16935  gsumpt  16988  gsum2dlem2  16998  dprdss  17076  dprd2dlem1  17090  dprd2da  17091  dmdprdsplit2lem  17094  lmhmpreima  17694  lmhmlsp  17695  psrelbasfun  18033  mplvalOLD  18085  mvrcl  18111  evlslem3  18183  evlseu  18185  mpfind  18205  gsumply1subr  18275  cygznlem2  18607  frlmup1  18832  frlmup4  18835  lindff1  18855  lindfrn  18856  iscnp3  19745  subbascn  19755  cnpnei  19765  cnclima  19769  iscncl  19770  cnclsi  19773  cncls  19775  cncnp  19781  cnrest2  19787  paste  19795  cnhaus  19855  bwthOLD  19911  conima  19926  1stcfb  19946  1stccnp  19963  1stckgenlem  20054  kgencn3  20059  txcnpi  20109  txcnp  20121  xkopt  20156  xkoco2cn  20159  xkococnlem  20160  hmeores  20272  fbasrn  20385  uzrest  20398  rnelfmlem  20453  rnelfm  20454  fmfnfmlem2  20456  fmfnfmlem3  20457  fmfnfmlem4  20458  fmfnfm  20459  cnflf2  20504  lmflf  20506  txflf  20507  cnextcn  20567  clssubg  20607  ghmcnp  20613  metcnp  21044  metustidOLD  21062  metustid  21063  metustsymOLD  21064  metustsym  21065  metustexhalfOLD  21066  metustexhalf  21067  cfilucfilOLD  21072  cfilucfil  21073  restmetu  21090  isngp2  21117  qtopbaslem  21265  tgqioo  21305  re2ndc  21306  bndth  21458  pi1xfrval  21554  pi1coval  21560  tchcph  21680  iscfil2  21705  rrxcph  21824  ovolficcss  21881  volf  21940  volsup  21966  uniioombllem3a  21993  uniioombllem4  21995  uniioombllem5  21996  dyadmbllem  22008  dyadmbl  22009  opnmbllem  22010  opnmblALT  22012  mbfimaicc  22040  ismbfd  22047  ismbf3d  22061  mbfimaopnlem  22062  mbfimaopn2  22064  i1fima  22085  i1fima2  22086  i1fd  22088  itg1addlem4  22106  ellimc2  22281  ellimc3  22283  dvres3  22317  dvres3a  22318  dvidlem  22319  dvcnp  22322  dvadd  22343  dvmul  22344  dvaddf  22345  dvmulf  22346  dvco  22350  dvcof  22351  dvcjbr  22352  dvcj  22353  dvrec  22358  dvcnvlem  22377  dvcnv  22378  dvef  22381  dvferm1  22386  dvferm2  22388  c1liplem1  22397  dvcnvrelem1  22418  dvcnvrelem2  22419  ftc1cn  22444  mdegldg  22466  mdegcl  22469  deg1n0ima  22489  plyco0  22589  plyeq0  22608  plypf1  22609  plyaddlem1  22610  plymullem1  22611  tayl0  22757  ulmdvlem3  22797  ulmdv  22798  pserdv  22824  dvlog  23032  efopn  23039  dchrelbas2  23512  dchrghm  23531  uhgrafun  24300  eupap1  24976  ghsubgolemOLD  25372  sspg  25641  ssps  25643  sspn  25649  htthlem  25834  issh2  26126  hlimuni  26156  hhsscms  26195  occllem  26221  occl  26222  chscllem4  26558  imaelshi  26977  fmptcof2  27502  curry2ima  27526  fpwrelmapffslem  27555  xrofsup  27582  xrge0tsmsd  27775  locfinreflem  27843  fsumcvg4  27932  zrhunitpreima  27959  esumpfinvallem  28080  imambfm  28233  sibfof  28282  sitgclg  28284  eulerpartlemd  28305  eulerpartlemt  28310  eulerpartlemmf  28314  eulerpartlemgvv  28315  eulerpartlemgu  28316  eulerpartlemgf  28318  dstrvprob  28410  dstfrvel  28412  orvclteinc  28414  erdszelem2  28636  erdszelem7  28641  erdszelem8  28642  cvmliftmolem1  28726  cvmliftlem3  28732  cvmliftlem10  28739  cvmliftlem13  28741  cvmliftlem15  28743  cvmlift2lem9  28756  cvmlift3lem6  28769  cvmlift3lem7  28770  mrsub0  28876  mrsubccat  28878  mrsubcn  28879  msubrn  28889  mclsax  28929  mthmblem  28940  mclsppslem  28943  mclspps  28944  nofun  29409  heicant  30049  opnmbllem0  30050  mblfinlem1  30051  dvtanlem  30064  itg2addnclem  30066  itg2addnclem2  30067  ftc1cnnc  30089  ftc1anclem7  30096  ftc1anc  30098  ftc2nc  30099  ivthALT  30153  indexdom  30225  cnres2  30259  heibor1lem  30305  grpokerinj  30347  elrfirn  30627  fnwe2lem2  30997  lmhmfgima  31030  fsuppeq  31043  arearect  31183  areaquad  31184  cncmpmax  31407  evthiccabs  31529  limccog  31626  cncficcgt0  31691  dvsinax  31708  fperdvper  31715  dirkercncflem2  31886  fourierdlem20  31909  fourierdlem42  31931  fourierdlem63  31952  fourierdlem76  31965  fourierdlem82  31971  fourierdlem93  31982  fourierdlem97  31986  fourierdlem113  32002  funfvima2d  37986
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 185  df-an 371  df-fn 5596  df-f 5597
  Copyright terms: Public domain W3C validator