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

Theorem fofun 6083
Description: An onto mapping is a function. (Contributed by NM, 29-Mar-2008.)
Assertion
Ref Expression
fofun (𝐹:𝐴onto𝐵 → Fun 𝐹)

Proof of Theorem fofun
StepHypRef Expression
1 fof 6082 . 2 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
21ffund 6016 1 (𝐹:𝐴onto𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 5851  ontowfo 5855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3567  df-ss 3574  df-fn 5860  df-f 5861  df-fo 5863
This theorem is referenced by:  foimacnv  6121  resdif  6124  fococnv2  6129  fornex  7097  fodomfi2  8843  fin1a2lem7  9188  brdom3  9310  1stf1  16772  1stf2  16773  2ndf1  16775  2ndf2  16776  1stfcl  16777  2ndfcl  16778  qtopcld  21456  qtopcmap  21462  elfm3  21694  bcthlem4  23064  uniiccdif  23286  grporn  27263  xppreima  29332  qtophaus  29727  bdayfun  31592  poimirlem26  33106  poimirlem27  33107  ovoliunnfl  33122  voliunnfl  33124
  Copyright terms: Public domain W3C validator