Theorem fofun 6719

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

Syntax hints:   → wi 4  Fun wfun 6452  –onto→wfo 6456

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 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-in 3899  df-ss 3909  df-fn 6461  df-f 6462  df-fo 6464

This theorem is referenced by:  foco  6732  foimacnv  6763  resdif  6767  fococnv2  6772  focdmex  7830  fodomfi2  9862  fin1a2lem7  10208  brdom3  10330  1stf1  17954  1stf2  17955  2ndf1  17957  2ndf2  17958  1stfcl  17959  2ndfcl  17960  qtopcld  22909  qtopcmap  22915  elfm3  23146  bcthlem4  24536  uniiccdif  24787  grporn  28928  xppreima  31028  fsuppcurry1  31105  fsuppcurry2  31106  qtophaus  31831  bdayimaon  33941  nosupno  33951  noinfno  33966  bdayfun  34012  noeta2  34024  poimirlem26  35847  poimirlem27  35848  ovoliunnfl  35863  voliunnfl  35865