Theorem fofun 6593

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

Syntax hints:   → wi 4  Fun wfun 6351  –onto→wfo 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-in 3945  df-ss 3954  df-fn 6360  df-f 6361  df-fo 6363

This theorem is referenced by:  foimacnv  6634  resdif  6637  fococnv2  6642  fornex  7659  fodomfi2  9488  fin1a2lem7  9830  brdom3  9952  1stf1  17444  1stf2  17445  2ndf1  17447  2ndf2  17448  1stfcl  17449  2ndfcl  17450  qtopcld  22323  qtopcmap  22329  elfm3  22560  bcthlem4  23932  uniiccdif  24181  grporn  28300  xppreima  30396  fsuppcurry1  30463  fsuppcurry2  30464  qtophaus  31102  bdayimaon  33199  nosupno  33205  bdayfun  33244  poimirlem26  34920  poimirlem27  34921  ovoliunnfl  34936  voliunnfl  34938