Theorem fofn 6774

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 6772	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
2	1	ffnd 6689	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 6506  –onto→wfo 6509

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 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931  df-f 6515  df-fo 6517

This theorem is referenced by:  fodmrnu  6780  foun  6818  fo00  6836  foelcdmi  6922  cbvfo  7264  foeqcnvco  7275  canth  7341  br1steqg  7990  br2ndeqg  7991  1stcof  7998  2ndcof  7999  df1st2  8077  df2nd2  8078  1stconst  8079  2ndconst  8080  fsplit  8096  smoiso2  8338  fodomfi  9261  fodomfiOLD  9281  brwdom2  9526  fodomfi2  10013  fpwwe  10599  imasaddfnlem  17491  imasvscafn  17500  imasleval  17504  dmaf  18011  cdaf  18012  imasmnd2  18701  imasgrp2  18987  efgrelexlemb  19680  efgredeu  19682  imasrng  20086  imasring  20239  znf1o  21461  zzngim  21462  indlcim  21749  1stcfb  23332  upxp  23510  uptx  23512  cnmpt1st  23555  cnmpt2nd  23556  qtoptopon  23591  qtopcld  23600  qtopeu  23603  qtoprest  23604  imastopn  23607  qtophmeo  23704  elfm3  23837  uniiccdif  25479  dirith  27440  nosupno  27615  nosupbday  27617  noinfno  27630  noinfbday  27632  noetasuplem4  27648  noetainflem4  27652  bdayfn  27685  grporn  30450  0vfval  30535  foresf1o  32433  2ndimaxp  32570  2ndresdju  32573  xppreima2  32575  1stpreimas  32629  1stpreima  32630  2ndpreima  32631  fsuppcurry1  32648  fsuppcurry2  32649  ffsrn  32652  gsummpt2d  32989  qusker  33320  imaslmod  33324  qtopt1  33825  qtophaus  33826  circcn  33828  cnre2csqima  33901  sigapildsys  34152  carsgclctunlem3  34311  fnbigcup  35889  filnetlem4  36369  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  ssnnf1octb  45188  nnfoctbdj  46454  fcoreslem4  47067  fcoresf1  47070  fargshiftfo  47443  fonex  48855