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

Theorem fofun 5796
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 5795 . 2  |-  ( F : A -onto-> B  ->  F : A --> B )
2 ffun 5733 . 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 5582   -->wf 5584   -onto->wfo 5586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490  df-fn 5591  df-f 5592  df-fo 5594
This theorem is referenced by:  foimacnv  5833  resdif  5836  fococnv2  5841  fornex  6753  fodomfi2  8441  fin1a2lem7  8786  brdom3  8906  1stf1  15319  1stf2  15320  2ndf1  15322  2ndf2  15323  1stfcl  15324  2ndfcl  15325  qtopcld  19977  qtopcmap  19983  elfm3  20214  bcthlem4  21529  uniiccdif  21750  grporn  24918  subgores  25010  xppreima  27187  qtophaus  27665  bdayfun  29041  ovoliunnfl  29661  voliunnfl  29663
  Copyright terms: Public domain W3C validator