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

Theorem fofun 5654
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 5653 . 2  |-  ( F : A -onto-> B  ->  F : A --> B )
2 ffun 5593 . 2  |-  ( F : A --> B  ->  Fun  F )
31, 2syl 16 1  |-  ( F : A -onto-> B  ->  Fun  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4   Fun wfun 5448   -->wf 5450   -onto->wfo 5452
This theorem is referenced by:  foimacnv  5692  resdif  5696  fococnv2  5701  fornex  5970  fodomfi2  7941  fin1a2lem7  8286  brdom3  8406  1stf1  14289  1stf2  14290  2ndf1  14292  2ndf2  14293  1stfcl  14294  2ndfcl  14295  qtopcld  17745  qtopcmap  17751  elfm3  17982  bcthlem4  19280  uniiccdif  19470  grporn  21800  subgores  21892  xppreima  24059  bdayfun  25631  ovoliunnfl  26248  voliunnfl  26250
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334  df-fn 5457  df-f 5458  df-fo 5460
  Copyright terms: Public domain W3C validator