Theorem fofun 6736

Description: An onto mapping is a function. (Contributed by NM, 29-Mar-2008.)

Assertion

Ref	Expression
fofun	⊢ (𝐹:𝐴–onto→𝐵 → Fun 𝐹)

Proof of Theorem fofun

Step	Hyp	Ref	Expression
1		fof 6735	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
2	1	ffund 6655	1 ⊢ (𝐹:𝐴–onto→𝐵 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 6475  –onto→wfo 6479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3919  df-fn 6484  df-f 6485  df-fo 6487

This theorem is referenced by:  foco  6749  foimacnv  6780  resdif  6784  fococnv2  6789  focdmex  7888  fodomfi2  9948  fin1a2lem7  10294  brdom3  10416  1stf1  18095  1stf2  18096  2ndf1  18098  2ndf2  18099  1stfcl  18100  2ndfcl  18101  qtopcld  23626  qtopcmap  23632  elfm3  23863  bcthlem4  25252  uniiccdif  25504  bdayimaon  27630  nosupno  27640  noinfno  27655  bdayfun  27709  noeta2  27722  precsexlem10  28152  precsexlem11  28153  grporn  30496  xppreima  32622  fsuppcurry1  32702  fsuppcurry2  32703  qtophaus  33844  poimirlem26  37685  poimirlem27  37686  ovoliunnfl  37701  voliunnfl  37703  fonex  48897