Theorem fofun 6685

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

Syntax hints:   → wi 4  Fun wfun 6424  –onto→wfo 6428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-ss 3908  df-fn 6433  df-f 6434  df-fo 6436

This theorem is referenced by:  foco  6698  foimacnv  6729  resdif  6732  fococnv2  6737  fornex  7785  fodomfi2  9800  fin1a2lem7  10146  brdom3  10268  1stf1  17890  1stf2  17891  2ndf1  17893  2ndf2  17894  1stfcl  17895  2ndfcl  17896  qtopcld  22845  qtopcmap  22851  elfm3  23082  bcthlem4  24472  uniiccdif  24723  grporn  28862  xppreima  30962  fsuppcurry1  31039  fsuppcurry2  31040  qtophaus  31765  bdayimaon  33875  nosupno  33885  noinfno  33900  bdayfun  33946  noeta2  33958  poimirlem26  35782  poimirlem27  35783  ovoliunnfl  35798  voliunnfl  35800