Theorem fofun 6747

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

Syntax hints:   → wi 4  Fun wfun 6486  –onto→wfo 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907  df-fn 6495  df-f 6496  df-fo 6498

This theorem is referenced by:  foco  6760  foimacnv  6791  resdif  6795  fococnv2  6800  focdmex  7902  fodomfi2  9973  fin1a2lem7  10319  brdom3  10441  1stf1  18149  1stf2  18150  2ndf1  18152  2ndf2  18153  1stfcl  18154  2ndfcl  18155  qtopcld  23688  qtopcmap  23694  elfm3  23925  bcthlem4  25304  uniiccdif  25555  bdayimaon  27671  nosupno  27681  noinfno  27696  bdayfun  27754  noeta2  27767  precsexlem10  28222  precsexlem11  28223  grporn  30607  xppreima  32733  fsuppcurry1  32812  fsuppcurry2  32813  qtophaus  33996  poimirlem26  37981  poimirlem27  37982  ovoliunnfl  37997  voliunnfl  37999  fonex  49354