Theorem fofun 6354

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

Syntax hints:   → wi 4  Fun wfun 6117  –onto→wfo 6121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-in 3805  df-ss 3812  df-fn 6126  df-f 6127  df-fo 6129

This theorem is referenced by:  foimacnv  6395  resdif  6398  fococnv2  6403  fornex  7397  fodomfi2  9196  fin1a2lem7  9543  brdom3  9665  1stf1  17185  1stf2  17186  2ndf1  17188  2ndf2  17189  1stfcl  17190  2ndfcl  17191  qtopcld  21887  qtopcmap  21893  elfm3  22124  bcthlem4  23495  uniiccdif  23744  grporn  27920  xppreima  29987  qtophaus  30437  bdayimaon  32371  nosupno  32377  bdayfun  32416  poimirlem26  33972  poimirlem27  33973  ovoliunnfl  33988  voliunnfl  33990