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

Theorem fofun 6354
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 6353 . 2 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
21ffund 6282 1 (𝐹:𝐴onto𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6117  ontowfo 6121
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-in 3805  df-ss 3812  df-fn 6126  df-f 6127  df-fo 6129
This theorem is referenced by:  foimacnv  6395  resdif  6398  fococnv2  6403  fornex  7397  fodomfi2  9196  fin1a2lem7  9543  brdom3  9665  1stf1  17185  1stf2  17186  2ndf1  17188  2ndf2  17189  1stfcl  17190  2ndfcl  17191  qtopcld  21887  qtopcmap  21893  elfm3  22124  bcthlem4  23495  uniiccdif  23744  grporn  27920  xppreima  29987  qtophaus  30437  bdayimaon  32371  nosupno  32377  bdayfun  32416  poimirlem26  33972  poimirlem27  33973  ovoliunnfl  33988  voliunnfl  33990
  Copyright terms: Public domain W3C validator