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

Theorem ffun 6086
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 6083 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fnfun 6026 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝐹:𝐴𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 5920   Fn wfn 5921  wf 5922
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 197  df-an 385  df-fn 5929  df-f 5930
This theorem is referenced by:  ffund  6087  funssxp  6099  f00  6125  fimacnv  6387  dff3  6412  fliftf  6605  fun11iun  7168  frnsuppeq  7352  smores2  7496  pmfun  7919  elmapfun  7923  pmresg  7927  fodomr  8152  ac6sfi  8245  fissuni  8312  fipreima  8313  fdmfifsupp  8326  frnfsuppbi  8345  fsuppmptif  8346  fsuppco2  8349  fsuppcor  8350  ordtypelem8  8471  ordtypelem9  8472  ordtypelem10  8473  unxpwdom2  8534  cnfcomlem  8634  tcrank  8785  fseqenlem2  8886  carduniima  8957  infmap2  9078  hsmexlem4  9289  hsmexlem5  9290  axdc3lem2  9311  axdc3lem4  9313  smobeth  9446  fpwwe2lem13  9502  fpwwe2  9503  inar1  9635  grur1  9680  nqerid  9793  zexALT  11434  hashkf  13159  hashgval  13160  revco  13626  ccatco  13627  lswco  13630  climdm  14329  isercolllem2  14440  isercolllem3  14441  isercoll  14442  sum0  14496  sumz  14497  fsumsers  14503  isumclim  14532  ntrivcvgfvn0  14675  ntrivcvgtail  14676  zprodn0  14713  iprodclim  14773  znnen  14985  mrcuni  16328  isacs2  16361  isacs5  17219  cntzmhm2  17818  frgpupval  18233  gsumzadd  18368  gsumpt  18407  gsum2dlem2  18416  dprdss  18474  dprd2dlem1  18486  dprd2da  18487  dmdprdsplit2lem  18490  lmhmpreima  19096  lmhmlsp  19097  psrelbasfun  19428  mvrcl  19497  evlseu  19564  mpfind  19584  gsumply1subr  19652  cygznlem2  19965  frlmup1  20185  frlmup4  20188  lindff1  20207  lindfrn  20208  iscnp3  21096  subbascn  21106  cnpnei  21116  cnclima  21120  iscncl  21121  cnclsi  21124  cncls  21126  cncnp  21132  cnrest2  21138  paste  21146  cnhaus  21206  connima  21276  1stcfb  21296  1stccnp  21313  1stckgenlem  21404  kgencn3  21409  txcnpi  21459  txcnp  21471  xkopt  21506  xkoco2cn  21509  xkococnlem  21510  hmeores  21622  fbasrn  21735  uzrest  21748  rnelfmlem  21803  rnelfm  21804  fmfnfmlem2  21806  fmfnfmlem3  21807  fmfnfmlem4  21808  fmfnfm  21809  cnflf2  21854  lmflf  21856  txflf  21857  cnextcn  21918  clssubg  21959  ghmcnp  21965  metcnp  22393  metustid  22406  metustsym  22407  metustexhalf  22408  cfilucfil  22411  restmetu  22422  isngp2  22448  qtopbaslem  22609  tgqioo  22650  re2ndc  22651  bndth  22804  pi1xfrval  22900  pi1coval  22906  tchcph  23082  iscfil2  23110  rrxcph  23226  ovolficcss  23284  volf  23343  volsup  23370  uniioombllem3a  23398  uniioombllem4  23400  uniioombllem5  23401  dyadmbllem  23413  dyadmbl  23414  opnmbllem  23415  opnmblALT  23417  mbfimaicc  23445  ismbfd  23452  ismbf3d  23466  mbfimaopnlem  23467  mbfimaopn2  23469  i1fima  23490  i1fima2  23491  i1fd  23493  itg1addlem4  23511  ellimc2  23686  ellimc3  23688  dvres3  23722  dvres3a  23723  dvidlem  23724  dvcnp  23727  dvadd  23748  dvmul  23749  dvaddf  23750  dvmulf  23751  dvco  23755  dvcof  23756  dvcjbr  23757  dvcj  23758  dvrec  23763  dvcnvlem  23784  dvcnv  23785  dvef  23788  dvferm1  23793  dvferm2  23795  c1liplem1  23804  dvcnvrelem1  23825  dvcnvrelem2  23826  ftc1cn  23851  mdegcl  23874  deg1n0ima  23894  plyco0  23993  plyeq0  24012  plypf1  24013  plyaddlem1  24014  plymullem1  24015  tayl0  24161  ulmdvlem3  24201  ulmdv  24202  pserdv  24228  dvlog  24442  efopn  24449  relogbf  24574  dchrelbas2  25007  dchrghm  25026  subusgr  26226  vdegp1ai  26488  wlkreslem  26622  pthdivtx  26681  pthdlem2lem  26719  sspg  27711  ssps  27713  sspn  27719  htthlem  27902  issh2  28194  hlimuni  28223  hhsscms  28264  occllem  28290  occl  28291  chscllem4  28627  imaelshi  29045  fmptcof2  29585  curry2ima  29614  fpwrelmapffslem  29635  xrofsup  29661  xrge0tsmsd  29913  smatrcl  29990  mdetpmtr1  30017  locfinreflem  30035  fsumcvg4  30124  zrhunitpreima  30150  esumpfinvallem  30264  imambfm  30452  carsggect  30508  sibfof  30530  sitgclg  30532  eulerpartlemd  30556  eulerpartlemt  30561  eulerpartlemmf  30565  eulerpartlemgvv  30566  eulerpartlemgu  30567  eulerpartlemgf  30569  dstrvprob  30661  dstfrvel  30663  orvclteinc  30665  rpsqrtcn  30799  erdszelem2  31300  erdszelem7  31305  erdszelem8  31306  cvmliftmolem1  31389  cvmliftlem3  31395  cvmliftlem10  31402  cvmliftlem13  31404  cvmliftlem15  31406  cvmlift2lem9  31419  cvmlift3lem6  31432  cvmlift3lem7  31433  mrsub0  31539  mrsubccat  31541  mrsubcn  31542  msubrn  31552  mclsax  31592  mthmblem  31603  mclsppslem  31606  mclspps  31607  nofun  31927  madeval  32060  ivthALT  32455  icoreunrn  33337  icoreelrn  33339  curf  33517  curunc  33521  heicant  33574  opnmbllem0  33575  mblfinlem1  33576  itg2addnclem  33591  itg2addnclem2  33592  ftc1cnnc  33614  ftc1anclem7  33621  ftc1anc  33623  ftc2nc  33624  indexdom  33659  cnres2  33692  heibor1lem  33738  grpokerinj  33822  elrfirn  37575  fnwe2lem2  37938  lmhmfgima  37971  arearect  38118  areaquad  38119  funfvima2d  38786  cncmpmax  39505  fidmfisupp  39704  absfun  39879  evthiccabs  40036  ioofun  40096  limccog  40170  cncficcgt0  40419  dvsinax  40445  fperdvper  40451  fvvolioof  40524  fvvolicof  40526  dirkercncflem2  40639  fourierdlem20  40662  fourierdlem42  40684  fourierdlem63  40704  fourierdlem76  40717  fourierdlem82  40723  fourierdlem93  40734  fourierdlem97  40738  fourierdlem113  40754  fge0iccico  40905  sge0sn  40914  sge0tsms  40915  sge0cl  40916  sge0f1o  40917  sge0isum  40962  ovolval3  41182  ovnovollem1  41191  pfxco  41763  fmtnoinf  41773  elbigolo1  42676
  Copyright terms: Public domain W3C validator