Theorem fofn 6756

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

Syntax hints:   → wi 4   Fn wfn 6495  –onto→wfo 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920  df-f 6504  df-fo 6506

This theorem is referenced by:  fodmrnu  6762  foun  6800  fo00  6818  foelcdmi  6903  cbvfo  7245  foeqcnvco  7256  canth  7322  br1steqg  7965  br2ndeqg  7966  1stcof  7973  2ndcof  7974  df1st2  8050  df2nd2  8051  1stconst  8052  2ndconst  8053  fsplit  8069  smoiso2  8311  fodomfi  9224  fodomfiOLD  9242  brwdom2  9490  fodomfi2  9982  fpwwe  10569  imasaddfnlem  17461  imasvscafn  17470  imasleval  17474  dmaf  17985  cdaf  17986  imasmnd2  18711  imasgrp2  18997  efgrelexlemb  19691  efgredeu  19693  imasrng  20124  imasring  20278  znf1o  21518  zzngim  21519  indlcim  21807  1stcfb  23401  upxp  23579  uptx  23581  cnmpt1st  23624  cnmpt2nd  23625  qtoptopon  23660  qtopcld  23669  qtopeu  23672  qtoprest  23673  imastopn  23676  qtophmeo  23773  elfm3  23906  uniiccdif  25547  dirith  27508  nosupno  27683  nosupbday  27685  noinfno  27698  noinfbday  27700  noetasuplem4  27716  noetainflem4  27720  bdayfn  27757  grporn  30608  0vfval  30693  foresf1o  32590  2ndimaxp  32735  2ndresdju  32738  xppreima2  32740  1stpreimas  32795  1stpreima  32796  2ndpreima  32797  fsuppcurry1  32813  fsuppcurry2  32814  ffsrn  32817  gsummpt2d  33142  qusker  33441  imaslmod  33445  qtopt1  34012  qtophaus  34013  circcn  34015  cnre2csqima  34088  sigapildsys  34339  carsgclctunlem3  34497  fnbigcup  36112  filnetlem4  36594  ovoliunnfl  37910  voliunnfl  37912  volsupnfl  37913  ssnnf1octb  45550  nnfoctbdj  46811  fcoreslem4  47423  fcoresf1  47426  fargshiftfo  47799  fonex  49223