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

Theorem fofun 6330
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 6329 . 2 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
21ffund 6258 1 (𝐹:𝐴onto𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6093  ontowfo 6097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-in 3774  df-ss 3781  df-fn 6102  df-f 6103  df-fo 6105
This theorem is referenced by:  foimacnv  6371  resdif  6374  fococnv2  6379  fornex  7368  fodomfi2  9167  fin1a2lem7  9514  brdom3  9636  1stf1  17144  1stf2  17145  2ndf1  17147  2ndf2  17148  1stfcl  17149  2ndfcl  17150  qtopcld  21842  qtopcmap  21848  elfm3  22079  bcthlem4  23450  uniiccdif  23683  grporn  27893  xppreima  29960  qtophaus  30411  bdayimaon  32348  nosupno  32354  bdayfun  32393  poimirlem26  33916  poimirlem27  33917  ovoliunnfl  33932  voliunnfl  33934
  Copyright terms: Public domain W3C validator