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

Theorem fofun 5811
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 5810 . 2  |-  ( F : A -onto-> B  ->  F : A --> B )
2 ffun 5748 . 2  |-  ( F : A --> B  ->  Fun  F )
31, 2syl 17 1  |-  ( F : A -onto-> B  ->  Fun  F )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   Fun wfun 5595   -->wf 5597   -onto->wfo 5599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456  df-fn 5604  df-f 5605  df-fo 5607
This theorem is referenced by:  foimacnv  5848  resdif  5851  fococnv2  5856  fornex  6776  fodomfi2  8489  fin1a2lem7  8834  brdom3  8954  1stf1  16028  1stf2  16029  2ndf1  16031  2ndf2  16032  1stfcl  16033  2ndfcl  16034  qtopcld  20659  qtopcmap  20665  elfm3  20896  bcthlem4  22188  uniiccdif  22412  grporn  25785  subgores  25877  xppreima  28088  qtophaus  28502  bdayfun  30350  poimirlem26  31669  poimirlem27  31670  ovoliunnfl  31685  voliunnfl  31687
  Copyright terms: Public domain W3C validator