Theorem fofn 6742

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

Syntax hints:   → wi 4   Fn wfn 6481  –onto→wfo 6484

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 3922  df-f 6490  df-fo 6492

This theorem is referenced by:  fodmrnu  6748  foun  6786  fo00  6804  foelcdmi  6888  cbvfo  7230  foeqcnvco  7241  canth  7307  br1steqg  7953  br2ndeqg  7954  1stcof  7961  2ndcof  7962  df1st2  8038  df2nd2  8039  1stconst  8040  2ndconst  8041  fsplit  8057  smoiso2  8299  fodomfi  9219  fodomfiOLD  9239  brwdom2  9484  fodomfi2  9973  fpwwe  10559  imasaddfnlem  17450  imasvscafn  17459  imasleval  17463  dmaf  17974  cdaf  17975  imasmnd2  18666  imasgrp2  18952  efgrelexlemb  19647  efgredeu  19649  imasrng  20080  imasring  20233  znf1o  21476  zzngim  21477  indlcim  21765  1stcfb  23348  upxp  23526  uptx  23528  cnmpt1st  23571  cnmpt2nd  23572  qtoptopon  23607  qtopcld  23616  qtopeu  23619  qtoprest  23620  imastopn  23623  qtophmeo  23720  elfm3  23853  uniiccdif  25495  dirith  27456  nosupno  27631  nosupbday  27633  noinfno  27646  noinfbday  27648  noetasuplem4  27664  noetainflem4  27668  bdayfn  27701  grporn  30483  0vfval  30568  foresf1o  32466  2ndimaxp  32603  2ndresdju  32606  xppreima2  32608  1stpreimas  32662  1stpreima  32663  2ndpreima  32664  fsuppcurry1  32681  fsuppcurry2  32682  ffsrn  32685  gsummpt2d  33015  qusker  33299  imaslmod  33303  qtopt1  33804  qtophaus  33805  circcn  33807  cnre2csqima  33880  sigapildsys  34131  carsgclctunlem3  34290  fnbigcup  35877  filnetlem4  36357  ovoliunnfl  37644  voliunnfl  37646  volsupnfl  37647  ssnnf1octb  45175  nnfoctbdj  46441  fcoreslem4  47054  fcoresf1  47057  fargshiftfo  47430  fonex  48855