Theorem fofun 6835

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

Syntax hints:   → wi 4  Fun wfun 6567  –onto→wfo 6571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993  df-fn 6576  df-f 6577  df-fo 6579

This theorem is referenced by:  foco  6848  foimacnv  6879  resdif  6883  fococnv2  6888  focdmex  7996  fodomfi2  10129  fin1a2lem7  10475  brdom3  10597  1stf1  18261  1stf2  18262  2ndf1  18264  2ndf2  18265  1stfcl  18266  2ndfcl  18267  qtopcld  23742  qtopcmap  23748  elfm3  23979  bcthlem4  25380  uniiccdif  25632  bdayimaon  27756  nosupno  27766  noinfno  27781  bdayfun  27835  noeta2  27847  precsexlem10  28258  precsexlem11  28259  grporn  30553  xppreima  32664  fsuppcurry1  32739  fsuppcurry2  32740  qtophaus  33782  poimirlem26  37606  poimirlem27  37607  ovoliunnfl  37622  voliunnfl  37624