Theorem fofun 6794

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6531  –onto→wfo 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ss 3919  df-fn 6540  df-f 6541  df-fo 6543

This theorem is used by:  foco  6807  foimacnv  6839  resdif  6843  fococnv2  6848  focdmex  7957  fodomfi2  10067  fin1a2lem7  10412  brdom3  10535  1stf1  18286  1stf2  18287  2ndf1  18289  2ndf2  18290  1stfcl  18291  2ndfcl  18292  qtopcld  23945  qtopcmap  23951  elfm3  24182  bcthlem4  25561  uniiccdif  25812  bdayimaon  27937  nosupno  27947  noinfno  27962  bdayfun  28020  noeta2  28034  precsexlem10  28489  precsexlem11  28490  grporn  31010  xppreima  33126  fsuppcurry1  33203  fsuppcurry2  33204  qtophaus  34354  onvfowev  35721  poimirlem26  38403  poimirlem27  38404  ovoliunnfl  38419  voliunnfl  38421  fonex  49803