Theorem fofun 6775

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

Syntax hints:   → wi 4  Fun wfun 6511  –onto→wfo 6515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3921  df-fn 6520  df-f 6521  df-fo 6523

This theorem is referenced by:  foco  6788  foimacnv  6820  resdif  6824  fococnv2  6829  focdmex  7933  fodomfi2  10013  fin1a2lem7  10360  brdom3  10482  1stf1  18207  1stf2  18208  2ndf1  18210  2ndf2  18211  1stfcl  18212  2ndfcl  18213  qtopcld  23753  qtopcmap  23759  elfm3  23990  bcthlem4  25369  uniiccdif  25620  bdayimaon  27734  nosupno  27744  noinfno  27759  bdayfun  27817  noeta2  27831  precsexlem10  28286  precsexlem11  28287  grporn  30670  xppreima  32797  fsuppcurry1  32876  fsuppcurry2  32877  qtophaus  34094  onvfowev  35423  poimirlem26  38109  poimirlem27  38110  ovoliunnfl  38125  voliunnfl  38127  fonex  49452