Theorem fofun 6741

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

Syntax hints:   → wi 4  Fun wfun 6480  –onto→wfo 6484

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 3922  df-fn 6489  df-f 6490  df-fo 6492

This theorem is referenced by:  foco  6754  foimacnv  6785  resdif  6789  fococnv2  6794  focdmex  7898  fodomfi2  9973  fin1a2lem7  10319  brdom3  10441  1stf1  18116  1stf2  18117  2ndf1  18119  2ndf2  18120  1stfcl  18121  2ndfcl  18122  qtopcld  23616  qtopcmap  23622  elfm3  23853  bcthlem4  25243  uniiccdif  25495  bdayimaon  27621  nosupno  27631  noinfno  27646  bdayfun  27700  noeta2  27713  precsexlem10  28141  precsexlem11  28142  grporn  30483  xppreima  32602  fsuppcurry1  32681  fsuppcurry2  32682  qtophaus  33802  poimirlem26  37625  poimirlem27  37626  ovoliunnfl  37641  voliunnfl  37643  fonex  48852