Theorem fofun 6116

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

Syntax hints:   → wi 4  Fun wfun 5882  –onto→wfo 5886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588  df-fn 5891  df-f 5892  df-fo 5894

This theorem is referenced by:  foimacnv  6154  resdif  6157  fococnv2  6162  fornex  7135  fodomfi2  8883  fin1a2lem7  9228  brdom3  9350  1stf1  16832  1stf2  16833  2ndf1  16835  2ndf2  16836  1stfcl  16837  2ndfcl  16838  qtopcld  21516  qtopcmap  21522  elfm3  21754  bcthlem4  23124  uniiccdif  23346  grporn  27375  xppreima  29449  qtophaus  29903  bdayimaon  31843  nosupno  31849  bdayfun  31888  poimirlem26  33435  poimirlem27  33436  ovoliunnfl  33451  voliunnfl  33453