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

Theorem fofun 5801
Description: An onto mapping is a function. (Contributed by NM, 29-Mar-2008.)
Assertion
Ref Expression
fofun

Proof of Theorem fofun
StepHypRef Expression
1 fof 5800 . 2
2 ffun 5738 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  Funwfun 5587  -->wf 5589  -onto->wfo 5591
This theorem is referenced by:  foimacnv  5838  resdif  5841  fococnv2  5846  fornex  6769  fodomfi2  8462  fin1a2lem7  8807  brdom3  8927  1stf1  15461  1stf2  15462  2ndf1  15464  2ndf2  15465  1stfcl  15466  2ndfcl  15467  qtopcld  20214  qtopcmap  20220  elfm3  20451  bcthlem4  21766  uniiccdif  21987  grporn  25214  subgores  25306  xppreima  27487  qtophaus  27839  bdayfun  29436  ovoliunnfl  30056  voliunnfl  30058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489  df-fn 5596  df-f 5597  df-fo 5599
  Copyright terms: Public domain W3C validator