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

Theorem fofun 5802
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 5801 . 2  |-  ( F : A -onto-> B  ->  F : A --> B )
2 ffun 5739 . 2  |-  ( F : A --> B  ->  Fun  F )
31, 2syl 16 1  |-  ( F : A -onto-> B  ->  Fun  F )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   Fun wfun 5588   -->wf 5590   -onto->wfo 5592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3478  df-ss 3485  df-fn 5597  df-f 5598  df-fo 5600
This theorem is referenced by:  foimacnv  5839  resdif  5842  fococnv2  5847  fornex  6768  fodomfi2  8458  fin1a2lem7  8803  brdom3  8923  1stf1  15588  1stf2  15589  2ndf1  15591  2ndf2  15592  1stfcl  15593  2ndfcl  15594  qtopcld  20340  qtopcmap  20346  elfm3  20577  bcthlem4  21892  uniiccdif  22113  grporn  25341  subgores  25433  xppreima  27635  qtophaus  28000  bdayfun  29653  ovoliunnfl  30261  voliunnfl  30263
  Copyright terms: Public domain W3C validator