Theorem fofun 6800

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6537  –onto→wfo 6541

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 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ss 3925  df-fn 6546  df-f 6547  df-fo 6549

This theorem is used by:  foco  6813  foimacnv  6845  resdif  6849  fococnv2  6854  focdmex  7962  fodomfi2  10063  fin1a2lem7  10408  brdom3  10530  1stf1  18273  1stf2  18274  2ndf1  18276  2ndf2  18277  1stfcl  18278  2ndfcl  18279  qtopcld  23907  qtopcmap  23913  elfm3  24144  bcthlem4  25523  uniiccdif  25774  bdayimaon  27894  nosupno  27904  noinfno  27919  bdayfun  27977  noeta2  27991  precsexlem10  28446  precsexlem11  28447  grporn  30910  xppreima  33027  fsuppcurry1  33106  fsuppcurry2  33107  qtophaus  34257  onvfowev  35624  poimirlem26  38338  poimirlem27  38339  ovoliunnfl  38354  voliunnfl  38356  fonex  49686