Theorem fofn 6674

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

Syntax hints:   → wi 4   Fn wfn 6413  –onto→wfo 6416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-f 6422  df-fo 6424

This theorem is referenced by:  fodmrnu  6680  foun  6718  fo00  6735  foelrni  6813  cbvfo  7141  foeqcnvco  7152  canth  7209  br1steqg  7826  br2ndeqg  7827  1stcof  7834  2ndcof  7835  df1st2  7909  df2nd2  7910  1stconst  7911  2ndconst  7912  fsplit  7928  fsplitOLD  7929  smoiso2  8171  fodomfi  9022  brwdom2  9262  fodomfi2  9747  fpwwe  10333  imasaddfnlem  17156  imasvscafn  17165  imasleval  17169  dmaf  17680  cdaf  17681  imasmnd2  18337  imasgrp2  18605  efgrelexlemb  19271  efgredeu  19273  imasring  19773  znf1o  20671  zzngim  20672  indlcim  20957  1stcfb  22504  upxp  22682  uptx  22684  cnmpt1st  22727  cnmpt2nd  22728  qtoptopon  22763  qtopcld  22772  qtopeu  22775  qtoprest  22776  imastopn  22779  qtophmeo  22876  elfm3  23009  uniiccdif  24647  dirith  26582  grporn  28784  0vfval  28869  foresf1o  30751  2ndimaxp  30885  2ndresdju  30887  xppreima2  30889  1stpreimas  30940  1stpreima  30941  2ndpreima  30942  fsuppcurry1  30962  fsuppcurry2  30963  ffsrn  30966  gsummpt2d  31211  qusker  31451  imaslmod  31455  qtopt1  31687  qtophaus  31688  circcn  31690  cnre2csqima  31763  sigapildsys  32030  carsgclctunlem3  32187  nosupno  33833  nosupbday  33835  noinfno  33848  noinfbday  33850  noetasuplem4  33866  noetainflem4  33870  bdayfn  33895  fnbigcup  34130  filnetlem4  34497  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  ssnnf1octb  42622  nnfoctbdj  43884  fcoreslem4  44447  fcoresf1  44450  fargshiftfo  44782