Theorem fofun 6741

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 6740	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
2	1	ffund 6660	1 ⊢ (𝐹:𝐴–onto→𝐵 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 6480  –onto→wfo 6484

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 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915  df-fn 6489  df-f 6490  df-fo 6492

This theorem is referenced by:  foco  6754  foimacnv  6785  resdif  6789  fococnv2  6794  focdmex  7894  fodomfi2  9958  fin1a2lem7  10304  brdom3  10426  1stf1  18100  1stf2  18101  2ndf1  18103  2ndf2  18104  1stfcl  18105  2ndfcl  18106  qtopcld  23629  qtopcmap  23635  elfm3  23866  bcthlem4  25255  uniiccdif  25507  bdayimaon  27633  nosupno  27643  noinfno  27658  bdayfun  27712  noeta2  27725  precsexlem10  28155  precsexlem11  28156  grporn  30503  xppreima  32629  fsuppcurry1  32711  fsuppcurry2  32712  qtophaus  33870  poimirlem26  37707  poimirlem27  37708  ovoliunnfl  37723  voliunnfl  37725  fonex  48992