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

Theorem ffun 6226
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 6223 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fnfun 6166 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝐹:𝐴𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6062   Fn wfn 6063  wf 6064
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 198  df-an 385  df-fn 6071  df-f 6072
This theorem is referenced by:  ffund  6227  funssxp  6243  f00  6269  fimacnv  6537  dff3  6562  fliftf  6757  fun11iun  7324  frnsuppeq  7509  pmfun  8080  pmresg  8088  fodomr  8318  ac6sfi  8411  fissuni  8478  fipreima  8479  frnfsuppbi  8511  cnfcomlem  8811  tcrank  8962  fseqenlem2  9099  carduniima  9170  infmap2  9293  hsmexlem4  9504  hsmexlem5  9505  axdc3lem2  9526  axdc3lem4  9528  smobeth  9661  fpwwe2lem13  9717  inar1  9850  grur1  9895  nqerid  10008  zexALT  11643  hashkf  13323  hashgval  13324  revco  13863  ccatco  13864  pfxco  13867  lswco  13868  climdm  14570  isercolllem2  14681  isercolllem3  14682  isercoll  14683  sum0  14737  sumz  14738  fsumsers  14744  isumclim  14773  ntrivcvgfvn0  14914  ntrivcvgtail  14915  zprodn0  14952  iprodclim  15011  znnen  15223  isacs2  16579  isacs5  17438  dprdss  18695  dprd2dlem1  18707  dmdprdsplit2lem  18711  iscnp3  21328  subbascn  21338  cnpnei  21348  cnclima  21352  iscncl  21353  cncls  21358  cnrest2  21370  cnhaus  21438  kgencn3  21641  xkopt  21738  xkococnlem  21742  hmeores  21854  fbasrn  21967  uzrest  21980  rnelfmlem  22035  rnelfm  22036  fmfnfmlem3  22039  fmfnfmlem4  22040  fmfnfm  22041  cnflf2  22086  metcnp  22625  metustsym  22639  cfilucfil  22643  restmetu  22654  qtopbaslem  22841  tgqioo  22882  re2ndc  22883  bndth  23036  tcphcph  23314  ovolficcss  23527  volf  23587  volsup  23614  uniioombllem3a  23642  uniioombllem4  23644  uniioombllem5  23645  dyadmbllem  23657  dyadmbl  23658  opnmbllem  23659  opnmblALT  23661  mbfimaicc  23689  ismbf3d  23712  mbfimaopnlem  23713  mbfimaopn2  23715  i1fima  23736  i1fima2  23737  i1fd  23739  itg1addlem4  23757  dvidlem  23970  dvcnp  23973  dvadd  23994  dvmul  23995  dvaddf  23996  dvmulf  23997  dvco  24001  dvcof  24002  dvcjbr  24003  dvcj  24004  dvrec  24009  dvcnvlem  24030  dvef  24034  dvferm1  24039  dvferm2  24041  c1liplem1  24050  dvcnvrelem2  24072  mdegcl  24120  deg1n0ima  24140  plyco0  24239  plypf1  24259  tayl0  24407  ulmdvlem3  24447  pserdv  24474  dvlog  24688  efopn  24695  relogbf  24820  subusgr  26460  wlkreslem  26858  pthdivtx  26917  pthdlem2lem  26955  issh2  28522  hlimuni  28551  hhsscms  28592  occllem  28618  occl  28619  chscllem4  28955  imaelshi  29373  xrofsup  29982  smatrcl  30309  mdetpmtr1  30336  locfinreflem  30354  fsumcvg4  30443  zrhunitpreima  30469  imambfm  30771  carsggect  30827  sibfof  30849  eulerpartlemt  30880  eulerpartlemmf  30884  eulerpartlemgvv  30885  eulerpartlemgf  30888  rpsqrtcn  31122  erdszelem2  31622  erdszelem7  31627  erdszelem8  31628  cvmliftlem15  31728  mrsub0  31861  mrsubccat  31863  mrsubcn  31864  mthmblem  31925  nofun  32246  madeval  32379  ivthALT  32773  icoreunrn  33640  icoreelrn  33642  curf  33811  curunc  33815  heicant  33868  opnmbllem0  33869  mblfinlem1  33870  itg2addnclem  33884  itg2addnclem2  33885  ftc1anclem7  33914  ftc1anc  33916  ftc2nc  33917  indexdom  33952  cnres2  33984  elrfirn  37936  fnwe2lem2  38298  arearect  38477  areaquad  38478  absfun  40204  evthiccabs  40360  ioofun  40416  cncficcgt0  40739  fperdvper  40771  fvvolioof  40843  fvvolicof  40845  fourierdlem20  40981  fourierdlem42  41003  fourierdlem63  41023  fourierdlem76  41036  fourierdlem93  41053  fourierdlem97  41057  fourierdlem113  41073  ovolval3  41501  fmtnoinf  42124  elbigolo1  43020
  Copyright terms: Public domain W3C validator