Theorem fofun 6797

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6532  –onto→wfo 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896  df-fn 6541  df-f 6542  df-fo 6544

This theorem is used by:  foco  6810  foimacnv  6842  resdif  6846  fococnv2  6851  focdmex  7968  fodomfi2  10142  fin1a2lem7  10487  brdom3  10610  1stf1  18371  1stf2  18372  2ndf1  18374  2ndf2  18375  1stfcl  18376  2ndfcl  18377  qtopcld  24037  qtopcmap  24043  elfm3  24274  bcthlem4  25653  uniiccdif  25904  bdayimaon  28055  nosupno  28065  noinfno  28080  bdayfun  28138  precsexlem10  28607  precsexlem11  28608  grporn  31128  xppreima  33286  fsuppcurry1  33362  fsuppcurry2  33363  qtophaus  34514  onvfowev  35969  poimirlem26  38657  poimirlem27  38658  ovoliunnfl  38673  voliunnfl  38675  fonex  50071