Theorem fofun 6807

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

Syntax hints:   → wi 4  Fun wfun 6538  –onto→wfo 6542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3956  df-ss 3966  df-fn 6547  df-f 6548  df-fo 6550

This theorem is referenced by:  foco  6820  foimacnv  6851  resdif  6855  fococnv2  6860  focdmex  7946  fodomfi2  10059  fin1a2lem7  10405  brdom3  10527  1stf1  18150  1stf2  18151  2ndf1  18153  2ndf2  18154  1stfcl  18155  2ndfcl  18156  qtopcld  23439  qtopcmap  23445  elfm3  23676  bcthlem4  25077  uniiccdif  25329  bdayimaon  27430  nosupno  27440  noinfno  27455  bdayfun  27508  noeta2  27520  precsexlem10  27899  precsexlem11  27900  grporn  30039  xppreima  32136  fsuppcurry1  32215  fsuppcurry2  32216  qtophaus  33112  poimirlem26  36819  poimirlem27  36820  ovoliunnfl  36835  voliunnfl  36837