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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907  df-fn 6495  df-f 6496  df-fo 6498

This theorem is referenced by:  foco  6760  foimacnv  6791  resdif  6795  fococnv2  6800  focdmex  7905  fodomfi2  9980  fin1a2lem7  10326  brdom3  10448  1stf1  18156  1stf2  18157  2ndf1  18159  2ndf2  18160  1stfcl  18161  2ndfcl  18162  qtopcld  23703  qtopcmap  23709  elfm3  23940  bcthlem4  25319  uniiccdif  25570  bdayimaon  27682  nosupno  27692  noinfno  27707  bdayfun  27765  noeta2  27778  precsexlem10  28233  precsexlem11  28234  grporn  30617  xppreima  32744  fsuppcurry1  32823  fsuppcurry2  32824  qtophaus  34027  poimirlem26  38020  poimirlem27  38021  ovoliunnfl  38036  voliunnfl  38038  fonex  49364