Theorem fofun 6747

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

Syntax hints:   → wi 4  Fun wfun 6486  –onto→wfo 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918  df-fn 6495  df-f 6496  df-fo 6498

This theorem is referenced by:  foco  6760  foimacnv  6791  resdif  6795  fococnv2  6800  focdmex  7900  fodomfi2  9970  fin1a2lem7  10316  brdom3  10438  1stf1  18115  1stf2  18116  2ndf1  18118  2ndf2  18119  1stfcl  18120  2ndfcl  18121  qtopcld  23657  qtopcmap  23663  elfm3  23894  bcthlem4  25283  uniiccdif  25535  bdayimaon  27661  nosupno  27671  noinfno  27686  bdayfun  27744  noeta2  27757  precsexlem10  28212  precsexlem11  28213  grporn  30596  xppreima  32723  fsuppcurry1  32803  fsuppcurry2  32804  qtophaus  33993  poimirlem26  37843  poimirlem27  37844  ovoliunnfl  37859  voliunnfl  37861  fonex  49108