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

Theorem fofn 5453
Description: An onto mapping is a function on its domain. (Contributed by NM, 16-Dec-2008.)
Assertion
Ref Expression
fofn  |-  ( F : A -onto-> B  ->  F  Fn  A )

Proof of Theorem fofn
StepHypRef Expression
1 fof 5451 . 2  |-  ( F : A -onto-> B  ->  F : A --> B )
2 ffn 5389 . 2  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 15 1  |-  ( F : A -onto-> B  ->  F  Fn  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    Fn wfn 5250   -->wf 5251   -onto->wfo 5253
This theorem is referenced by:  fodmrnu  5459  foun  5491  fo00  5509  cbvfo  5799  foeqcnvco  5804  1stcof  6147  2ndcof  6148  df1st2  6205  df2nd2  6206  1stconst  6207  2ndconst  6208  fsplit  6223  canth  6294  smoiso2  6386  fodomfi  7135  brwdom2  7287  fodomfi2  7687  fpwwe  8268  imasaddfnlem  13430  imasvscafn  13439  imasleval  13443  dmaf  13881  cdaf  13882  imasmnd2  14409  imasgrp2  14610  efgrelexlemb  15059  efgredeu  15061  imasrng  15402  znf1o  16505  zzngim  16506  1stcfb  17171  upxp  17317  uptx  17319  cnmpt1st  17362  cnmpt2nd  17363  qtoptopon  17395  qtopcld  17404  qtopeu  17407  qtoprest  17408  imastopn  17411  qtophmeo  17508  elfm3  17645  uniiccdif  18933  dirith  20678  grporn  20879  subgores  20971  vcoprnelem  21134  0vfval  21162  xppreima2  23212  cnre2csqima  23295  br1steq  24130  br2ndeq  24131  fnbigcup  24441  prj1b  25079  prj3  25080  imfstnrelc  25081  filnetlem4  26330  indlcim  27310
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166  df-f 5259  df-fo 5261
  Copyright terms: Public domain W3C validator