Theorem fofun 6791

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

Syntax hints:   → wi 4  Fun wfun 6525  –onto→wfo 6529

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 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ss 3943  df-fn 6534  df-f 6535  df-fo 6537

This theorem is referenced by:  foco  6804  foimacnv  6835  resdif  6839  fococnv2  6844  focdmex  7954  fodomfi2  10074  fin1a2lem7  10420  brdom3  10542  1stf1  18204  1stf2  18205  2ndf1  18207  2ndf2  18208  1stfcl  18209  2ndfcl  18210  qtopcld  23651  qtopcmap  23657  elfm3  23888  bcthlem4  25279  uniiccdif  25531  bdayimaon  27657  nosupno  27667  noinfno  27682  bdayfun  27736  noeta2  27748  precsexlem10  28170  precsexlem11  28171  grporn  30502  xppreima  32623  fsuppcurry1  32702  fsuppcurry2  32703  qtophaus  33867  poimirlem26  37670  poimirlem27  37671  ovoliunnfl  37686  voliunnfl  37688  fonex  48842