Theorem fofun 6806

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

Syntax hints:   → wi 4  Fun wfun 6537  –onto→wfo 6541

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-fn 6546  df-f 6547  df-fo 6549

This theorem is referenced by:  foco  6819  foimacnv  6850  resdif  6854  fococnv2  6859  focdmex  7941  fodomfi2  10054  fin1a2lem7  10400  brdom3  10522  1stf1  18143  1stf2  18144  2ndf1  18146  2ndf2  18147  1stfcl  18148  2ndfcl  18149  qtopcld  23216  qtopcmap  23222  elfm3  23453  bcthlem4  24843  uniiccdif  25094  bdayimaon  27193  nosupno  27203  noinfno  27218  bdayfun  27271  noeta2  27283  precsexlem10  27659  precsexlem11  27660  grporn  29769  xppreima  31866  fsuppcurry1  31945  fsuppcurry2  31946  qtophaus  32811  poimirlem26  36509  poimirlem27  36510  ovoliunnfl  36525  voliunnfl  36527