Theorem fofn 6732

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

Syntax hints:   → wi 4   Fn wfn 6471  –onto→wfo 6474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3914  df-f 6480  df-fo 6482

This theorem is referenced by:  fodmrnu  6738  foun  6776  fo00  6794  foelcdmi  6878  cbvfo  7218  foeqcnvco  7229  canth  7295  br1steqg  7938  br2ndeqg  7939  1stcof  7946  2ndcof  7947  df1st2  8023  df2nd2  8024  1stconst  8025  2ndconst  8026  fsplit  8042  smoiso2  8284  fodomfi  9191  fodomfiOLD  9209  brwdom2  9454  fodomfi2  9946  fpwwe  10532  imasaddfnlem  17427  imasvscafn  17436  imasleval  17440  dmaf  17951  cdaf  17952  imasmnd2  18677  imasgrp2  18963  efgrelexlemb  19657  efgredeu  19659  imasrng  20090  imasring  20243  znf1o  21483  zzngim  21484  indlcim  21772  1stcfb  23355  upxp  23533  uptx  23535  cnmpt1st  23578  cnmpt2nd  23579  qtoptopon  23614  qtopcld  23623  qtopeu  23626  qtoprest  23627  imastopn  23630  qtophmeo  23727  elfm3  23860  uniiccdif  25501  dirith  27462  nosupno  27637  nosupbday  27639  noinfno  27652  noinfbday  27654  noetasuplem4  27670  noetainflem4  27674  bdayfn  27707  grporn  30493  0vfval  30578  foresf1o  32476  2ndimaxp  32620  2ndresdju  32623  xppreima2  32625  1stpreimas  32679  1stpreima  32680  2ndpreima  32681  fsuppcurry1  32699  fsuppcurry2  32700  ffsrn  32703  gsummpt2d  33021  qusker  33306  imaslmod  33310  qtopt1  33840  qtophaus  33841  circcn  33843  cnre2csqima  33916  sigapildsys  34167  carsgclctunlem3  34325  fnbigcup  35935  filnetlem4  36415  ovoliunnfl  37702  voliunnfl  37704  volsupnfl  37705  ssnnf1octb  45231  nnfoctbdj  46494  fcoreslem4  47097  fcoresf1  47100  fargshiftfo  47473  fonex  48898