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

Theorem fofun 5452
Description: An onto mapping is a function. (Contributed by NM, 29-Mar-2008.)
Assertion
Ref Expression
fofun  |-  ( F : A -onto-> B  ->  Fun  F )

Proof of Theorem fofun
StepHypRef Expression
1 fof 5451 . 2  |-  ( F : A -onto-> B  ->  F : A --> B )
2 ffun 5391 . 2  |-  ( F : A --> B  ->  Fun  F )
31, 2syl 15 1  |-  ( F : A -onto-> B  ->  Fun  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4   Fun wfun 5249   -->wf 5251   -onto->wfo 5253
This theorem is referenced by:  foimacnv  5490  resdif  5494  fococnv2  5499  fornex  5750  fodomfi2  7687  fin1a2lem7  8032  brdom3  8153  1stf1  13966  1stf2  13967  2ndf1  13969  2ndf2  13970  1stfcl  13971  2ndfcl  13972  qtopcld  17404  qtopcmap  17410  elfm3  17645  bcthlem4  18749  uniiccdif  18933  grporn  20879  subgores  20971  xppreima  23211  bdayfun  24330  imfstnrelc  25081  domrancur1clem  25201  domrancur1c  25202  svs2  25487
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-fn 5258  df-f 5259  df-fo 5261
  Copyright terms: Public domain W3C validator