Theorem fofun 6776

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

Syntax hints:   → wi 4  Fun wfun 6508  –onto→wfo 6512

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 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934  df-fn 6517  df-f 6518  df-fo 6520

This theorem is referenced by:  foco  6789  foimacnv  6820  resdif  6824  fococnv2  6829  focdmex  7937  fodomfi2  10020  fin1a2lem7  10366  brdom3  10488  1stf1  18160  1stf2  18161  2ndf1  18163  2ndf2  18164  1stfcl  18165  2ndfcl  18166  qtopcld  23607  qtopcmap  23613  elfm3  23844  bcthlem4  25234  uniiccdif  25486  bdayimaon  27612  nosupno  27622  noinfno  27637  bdayfun  27691  noeta2  27703  precsexlem10  28125  precsexlem11  28126  grporn  30457  xppreima  32576  fsuppcurry1  32655  fsuppcurry2  32656  qtophaus  33833  poimirlem26  37647  poimirlem27  37648  ovoliunnfl  37663  voliunnfl  37665  fonex  48859