Theorem fofun 6822

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6555  ⟶ontowfo 6559

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901  df-fn 6564  df-f 6565  df-fo 6567

This theorem is used by:  foco  6835  foimacnv  6867  resdif  6871  fococnv2  6877  focdmex  7995  fodomfi2  10169  fin1a2lem7  10514  brdom3  10637  1stf1  18398  1stf2  18399  2ndf1  18401  2ndf2  18402  1stfcl  18403  2ndfcl  18404  qtopcld  24065  qtopcmap  24071  elfm3  24302  bcthlem4  25681  uniiccdif  25932  bdayimaon  28083  nosupno  28093  noinfno  28108  bdayfun  28166  precsexlem10  28635  precsexlem11  28636  grporn  31156  xppreima  33314  fsuppcurry1  33389  fsuppcurry2  33390  qtophaus  34551  onvfowev  36063  poimirlem26  38769  poimirlem27  38770  ovoliunnfl  38785  voliunnfl  38787  fonex  50193