Theorem fofun 6773

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

Syntax hints:   → wi 4  Fun wfun 6505  –onto→wfo 6509

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 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931  df-fn 6514  df-f 6515  df-fo 6517

This theorem is referenced by:  foco  6786  foimacnv  6817  resdif  6821  fococnv2  6826  focdmex  7934  fodomfi2  10013  fin1a2lem7  10359  brdom3  10481  1stf1  18153  1stf2  18154  2ndf1  18156  2ndf2  18157  1stfcl  18158  2ndfcl  18159  qtopcld  23600  qtopcmap  23606  elfm3  23837  bcthlem4  25227  uniiccdif  25479  bdayimaon  27605  nosupno  27615  noinfno  27630  bdayfun  27684  noeta2  27696  precsexlem10  28118  precsexlem11  28119  grporn  30450  xppreima  32569  fsuppcurry1  32648  fsuppcurry2  32649  qtophaus  33826  poimirlem26  37640  poimirlem27  37641  ovoliunnfl  37656  voliunnfl  37658  fonex  48855