Theorem fofun 6795

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

Syntax hints:   → wi 4  Fun wfun 6532  –onto→wfo 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923  df-fn 6541  df-f 6542  df-fo 6544

This theorem is referenced by:  foco  6808  foimacnv  6840  resdif  6844  fococnv2  6849  focdmex  7954  fodomfi2  10045  fin1a2lem7  10391  brdom3  10513  1stf1  18249  1stf2  18250  2ndf1  18252  2ndf2  18253  1stfcl  18254  2ndfcl  18255  qtopcld  23851  qtopcmap  23857  elfm3  24088  bcthlem4  25467  uniiccdif  25718  bdayimaon  27835  nosupno  27845  noinfno  27860  bdayfun  27918  noeta2  27932  precsexlem10  28387  precsexlem11  28388  grporn  30851  xppreima  32968  fsuppcurry1  33047  fsuppcurry2  33048  qtophaus  34204  onvfowev  35578  poimirlem26  38275  poimirlem27  38276  ovoliunnfl  38291  voliunnfl  38293  fonex  49622