Theorem fofun 6755

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

Syntax hints:   → wi 4  Fun wfun 6494  –onto→wfo 6498

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920  df-fn 6503  df-f 6504  df-fo 6506

This theorem is referenced by:  foco  6768  foimacnv  6799  resdif  6803  fococnv2  6808  focdmex  7910  fodomfi2  9982  fin1a2lem7  10328  brdom3  10450  1stf1  18127  1stf2  18128  2ndf1  18130  2ndf2  18131  1stfcl  18132  2ndfcl  18133  qtopcld  23669  qtopcmap  23675  elfm3  23906  bcthlem4  25295  uniiccdif  25547  bdayimaon  27673  nosupno  27683  noinfno  27698  bdayfun  27756  noeta2  27769  precsexlem10  28224  precsexlem11  28225  grporn  30608  xppreima  32734  fsuppcurry1  32813  fsuppcurry2  32814  qtophaus  34013  poimirlem26  37891  poimirlem27  37892  ovoliunnfl  37907  voliunnfl  37909  fonex  49220