Theorem fofn 6741

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

Syntax hints:   → wi 4   Fn wfn 6480  –onto→wfo 6483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900  df-f 6489  df-fo 6491

This theorem is referenced by:  fodmrnu  6747  foun  6785  fo00  6803  foelcdmi  6888  cbvfo  7233  foeqcnvco  7244  canth  7310  br1steqg  7953  br2ndeqg  7954  1stcof  7961  2ndcof  7962  df1st2  8037  df2nd2  8038  1stconst  8039  2ndconst  8040  fsplit  8056  smoiso2  8299  fodomfi  9212  fodomfiOLD  9230  brwdom2  9478  fodomfi2  9973  fpwwe  10560  imasaddfnlem  17483  imasvscafn  17492  imasleval  17496  dmaf  18007  cdaf  18008  imasmnd2  18733  imasgrp2  19022  efgrelexlemb  19716  efgredeu  19718  imasrng  20149  imasring  20301  znf1o  21526  zzngim  21527  indlcim  21815  1stcfb  23428  upxp  23606  uptx  23608  cnmpt1st  23651  cnmpt2nd  23652  qtoptopon  23687  qtopcld  23696  qtopeu  23699  qtoprest  23700  imastopn  23703  qtophmeo  23800  elfm3  23933  uniiccdif  25563  dirith  27510  nosupno  27685  nosupbday  27687  noinfno  27700  noinfbday  27702  noetasuplem4  27718  noetainflem4  27722  bdayfn  27759  grporn  30610  0vfval  30695  foresf1o  32592  2ndimaxp  32738  2ndresdju  32741  xppreima2  32743  1stpreimas  32798  1stpreima  32799  2ndpreima  32800  fsuppcurry1  32816  fsuppcurry2  32817  ffsrn  32820  gsummpt2d  33130  qusker  33432  imaslmod  33436  qtopt1  34019  qtophaus  34020  circcn  34022  cnre2csqima  34095  sigapildsys  34346  carsgclctunlem3  34504  fnbigcup  36127  filnetlem4  36609  ovoliunnfl  38029  voliunnfl  38031  volsupnfl  38032  ssnnf1octb  45641  nnfoctbdj  46899  fcoreslem4  47529  fcoresf1  47532  fargshiftfo  47917  fonex  49357