Theorem fofun 6822

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

Syntax hints:   → wi 4  Fun wfun 6557  –onto→wfo 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ss 3980  df-fn 6566  df-f 6567  df-fo 6569

This theorem is referenced by:  foco  6835  foimacnv  6866  resdif  6870  fococnv2  6875  focdmex  7979  fodomfi2  10098  fin1a2lem7  10444  brdom3  10566  1stf1  18248  1stf2  18249  2ndf1  18251  2ndf2  18252  1stfcl  18253  2ndfcl  18254  qtopcld  23737  qtopcmap  23743  elfm3  23974  bcthlem4  25375  uniiccdif  25627  bdayimaon  27753  nosupno  27763  noinfno  27778  bdayfun  27832  noeta2  27844  precsexlem10  28255  precsexlem11  28256  grporn  30550  xppreima  32662  fsuppcurry1  32743  fsuppcurry2  32744  qtophaus  33797  poimirlem26  37633  poimirlem27  37634  ovoliunnfl  37649  voliunnfl  37651