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

Theorem fofun 6564
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 6563 . 2 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
21ffund 6491 1 (𝐹:𝐴onto𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6322  ontowfo 6326
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-v 3473  df-in 3917  df-ss 3927  df-fn 6331  df-f 6332  df-fo 6334
This theorem is referenced by:  foimacnv  6605  resdif  6608  fococnv2  6613  fornex  7632  fodomfi2  9463  fin1a2lem7  9805  brdom3  9927  1stf1  17420  1stf2  17421  2ndf1  17423  2ndf2  17424  1stfcl  17425  2ndfcl  17426  qtopcld  22296  qtopcmap  22302  elfm3  22533  bcthlem4  23909  uniiccdif  24160  grporn  28282  xppreima  30380  fsuppcurry1  30447  fsuppcurry2  30448  qtophaus  31110  bdayimaon  33204  nosupno  33210  bdayfun  33249  poimirlem26  34963  poimirlem27  34964  ovoliunnfl  34979  voliunnfl  34981
  Copyright terms: Public domain W3C validator