Theorem fofun 6789

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6525  –onto→wfo 6529

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916  df-fn 6534  df-f 6535  df-fo 6537

This theorem is used by:  foco  6802  foimacnv  6834  resdif  6838  fococnv2  6843  focdmex  7957  fodomfi2  10120  fin1a2lem7  10465  brdom3  10588  1stf1  18346  1stf2  18347  2ndf1  18349  2ndf2  18350  1stfcl  18351  2ndfcl  18352  qtopcld  24012  qtopcmap  24018  elfm3  24249  bcthlem4  25628  uniiccdif  25879  bdayimaon  28032  nosupno  28042  noinfno  28057  bdayfun  28115  noeta2  28129  precsexlem10  28584  precsexlem11  28585  grporn  31105  xppreima  33221  fsuppcurry1  33298  fsuppcurry2  33299  qtophaus  34450  onvfowev  35868  poimirlem26  38532  poimirlem27  38533  ovoliunnfl  38548  voliunnfl  38550  fonex  49921