Theorem fofun 6783

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

Syntax hints:   → wi 4  Fun wfun 6519  –onto→wfo 6523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924  df-fn 6528  df-f 6529  df-fo 6531

This theorem is referenced by:  foco  6796  foimacnv  6828  resdif  6832  fococnv2  6837  focdmex  7941  fodomfi2  10032  fin1a2lem7  10378  brdom3  10500  1stf1  18238  1stf2  18239  2ndf1  18241  2ndf2  18242  1stfcl  18243  2ndfcl  18244  qtopcld  23831  qtopcmap  23837  elfm3  24068  bcthlem4  25447  uniiccdif  25698  bdayimaon  27815  nosupno  27825  noinfno  27840  bdayfun  27898  noeta2  27912  precsexlem10  28367  precsexlem11  28368  grporn  30782  xppreima  32902  fsuppcurry1  32981  fsuppcurry2  32982  qtophaus  34143  onvfowev  35471  poimirlem26  38157  poimirlem27  38158  ovoliunnfl  38173  voliunnfl  38175  fonex  49496