Theorem fofun 6753

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

Syntax hints:   → wi 4  Fun wfun 6492  –onto→wfo 6496

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906  df-fn 6501  df-f 6502  df-fo 6504

This theorem is referenced by:  foco  6766  foimacnv  6797  resdif  6801  fococnv2  6806  focdmex  7909  fodomfi2  9982  fin1a2lem7  10328  brdom3  10450  1stf1  18158  1stf2  18159  2ndf1  18161  2ndf2  18162  1stfcl  18163  2ndfcl  18164  qtopcld  23678  qtopcmap  23684  elfm3  23915  bcthlem4  25294  uniiccdif  25545  bdayimaon  27657  nosupno  27667  noinfno  27682  bdayfun  27740  noeta2  27753  precsexlem10  28208  precsexlem11  28209  grporn  30592  xppreima  32718  fsuppcurry1  32797  fsuppcurry2  32798  qtophaus  33980  poimirlem26  37967  poimirlem27  37968  ovoliunnfl  37983  voliunnfl  37985  fonex  49342