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

Theorem fofun 6279
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 6278 . 2 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
21ffund 6211 1 (𝐹:𝐴onto𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6044  ontowfo 6048
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-in 3723  df-ss 3730  df-fn 6053  df-f 6054  df-fo 6056
This theorem is referenced by:  foimacnv  6317  resdif  6320  fococnv2  6325  fornex  7302  fodomfi2  9094  fin1a2lem7  9441  brdom3  9563  1stf1  17054  1stf2  17055  2ndf1  17057  2ndf2  17058  1stfcl  17059  2ndfcl  17060  qtopcld  21739  qtopcmap  21745  elfm3  21976  bcthlem4  23345  uniiccdif  23567  grporn  27706  xppreima  29780  qtophaus  30234  bdayimaon  32171  nosupno  32177  bdayfun  32216  poimirlem26  33767  poimirlem27  33768  ovoliunnfl  33783  voliunnfl  33785
  Copyright terms: Public domain W3C validator