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

Theorem fofun 6821
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 6820 . 2 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
21ffund 6740 1 (𝐹:𝐴onto𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6555  ontowfo 6559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968  df-fn 6564  df-f 6565  df-fo 6567
This theorem is referenced by:  foco  6834  foimacnv  6865  resdif  6869  fococnv2  6874  focdmex  7980  fodomfi2  10100  fin1a2lem7  10446  brdom3  10568  1stf1  18237  1stf2  18238  2ndf1  18240  2ndf2  18241  1stfcl  18242  2ndfcl  18243  qtopcld  23721  qtopcmap  23727  elfm3  23958  bcthlem4  25361  uniiccdif  25613  bdayimaon  27738  nosupno  27748  noinfno  27763  bdayfun  27817  noeta2  27829  precsexlem10  28240  precsexlem11  28241  grporn  30540  xppreima  32655  fsuppcurry1  32736  fsuppcurry2  32737  qtophaus  33835  poimirlem26  37653  poimirlem27  37654  ovoliunnfl  37669  voliunnfl  37671
  Copyright terms: Public domain W3C validator