Theorem fofun 6594

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

Syntax hints:   → wi 4  Fun wfun 6352  –onto→wfo 6356

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-in 3946  df-ss 3955  df-fn 6361  df-f 6362  df-fo 6364

This theorem is referenced by:  foimacnv  6635  resdif  6638  fococnv2  6643  fornex  7660  fodomfi2  9489  fin1a2lem7  9831  brdom3  9953  1stf1  17445  1stf2  17446  2ndf1  17448  2ndf2  17449  1stfcl  17450  2ndfcl  17451  qtopcld  22324  qtopcmap  22330  elfm3  22561  bcthlem4  23933  uniiccdif  24182  grporn  28301  xppreima  30397  fsuppcurry1  30464  fsuppcurry2  30465  qtophaus  31104  bdayimaon  33201  nosupno  33207  bdayfun  33246  poimirlem26  34922  poimirlem27  34923  ovoliunnfl  34938  voliunnfl  34940