Theorem fofun 6279

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

Syntax hints:   → wi 4  Fun wfun 6044  –onto→wfo 6048

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-in 3723  df-ss 3730  df-fn 6053  df-f 6054  df-fo 6056

This theorem is referenced by:  foimacnv  6317  resdif  6320  fococnv2  6325  fornex  7302  fodomfi2  9094  fin1a2lem7  9441  brdom3  9563  1stf1  17054  1stf2  17055  2ndf1  17057  2ndf2  17058  1stfcl  17059  2ndfcl  17060  qtopcld  21739  qtopcmap  21745  elfm3  21976  bcthlem4  23345  uniiccdif  23567  grporn  27706  xppreima  29780  qtophaus  30234  bdayimaon  32171  nosupno  32177  bdayfun  32216  poimirlem26  33767  poimirlem27  33768  ovoliunnfl  33783  voliunnfl  33785