Theorem fofun 6821

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

Syntax hints:   → wi 4  Fun wfun 6555  –onto→wfo 6559

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 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968  df-fn 6564  df-f 6565  df-fo 6567

This theorem is referenced by:  foco  6834  foimacnv  6865  resdif  6869  fococnv2  6874  focdmex  7980  fodomfi2  10100  fin1a2lem7  10446  brdom3  10568  1stf1  18237  1stf2  18238  2ndf1  18240  2ndf2  18241  1stfcl  18242  2ndfcl  18243  qtopcld  23721  qtopcmap  23727  elfm3  23958  bcthlem4  25361  uniiccdif  25613  bdayimaon  27738  nosupno  27748  noinfno  27763  bdayfun  27817  noeta2  27829  precsexlem10  28240  precsexlem11  28241  grporn  30540  xppreima  32655  fsuppcurry1  32736  fsuppcurry2  32737  qtophaus  33835  poimirlem26  37653  poimirlem27  37654  ovoliunnfl  37669  voliunnfl  37671