Theorem fofn 6808

Description: An onto mapping is a function on its domain. (Contributed by NM, 16-Dec-2008.)

Assertion

Ref	Expression
fofn	⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴)

Proof of Theorem fofn

Step	Hyp	Ref	Expression
1		fof 6806	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
2	1	ffnd 6719	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 6539  –onto→wfo 6542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-f 6548  df-fo 6550

This theorem is referenced by:  fodmrnu  6814  foun  6852  fo00  6870  foelcdmi  6954  cbvfo  7287  foeqcnvco  7298  canth  7362  br1steqg  7997  br2ndeqg  7998  1stcof  8005  2ndcof  8006  df1st2  8084  df2nd2  8085  1stconst  8086  2ndconst  8087  fsplit  8103  smoiso2  8369  fodomfi  9325  brwdom2  9568  fodomfi2  10055  fpwwe  10641  imasaddfnlem  17474  imasvscafn  17483  imasleval  17487  dmaf  17999  cdaf  18000  imasmnd2  18662  imasgrp2  18938  efgrelexlemb  19618  efgredeu  19620  imasring  20143  znf1o  21107  zzngim  21108  indlcim  21395  1stcfb  22949  upxp  23127  uptx  23129  cnmpt1st  23172  cnmpt2nd  23173  qtoptopon  23208  qtopcld  23217  qtopeu  23220  qtoprest  23221  imastopn  23224  qtophmeo  23321  elfm3  23454  uniiccdif  25095  dirith  27032  nosupno  27206  nosupbday  27208  noinfno  27221  noinfbday  27223  noetasuplem4  27239  noetainflem4  27243  bdayfn  27275  grporn  29774  0vfval  29859  foresf1o  31742  2ndimaxp  31872  2ndresdju  31874  xppreima2  31876  1stpreimas  31927  1stpreima  31928  2ndpreima  31929  fsuppcurry1  31950  fsuppcurry2  31951  ffsrn  31954  gsummpt2d  32201  qusker  32464  imaslmod  32468  qtopt1  32815  qtophaus  32816  circcn  32818  cnre2csqima  32891  sigapildsys  33160  carsgclctunlem3  33319  fnbigcup  34873  filnetlem4  35266  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  ssnnf1octb  43893  nnfoctbdj  45172  fcoreslem4  45776  fcoresf1  45779  fargshiftfo  46110  imasrng  46678