Theorem fofn 6754

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

Syntax hints:   → wi 4   Fn wfn 6493  –onto→wfo 6496

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906  df-f 6502  df-fo 6504

This theorem is referenced by:  fodmrnu  6760  foun  6798  fo00  6816  foelcdmi  6901  cbvfo  7244  foeqcnvco  7255  canth  7321  br1steqg  7964  br2ndeqg  7965  1stcof  7972  2ndcof  7973  df1st2  8048  df2nd2  8049  1stconst  8050  2ndconst  8051  fsplit  8067  smoiso2  8309  fodomfi  9222  fodomfiOLD  9240  brwdom2  9488  fodomfi2  9982  fpwwe  10569  imasaddfnlem  17492  imasvscafn  17501  imasleval  17505  dmaf  18016  cdaf  18017  imasmnd2  18742  imasgrp2  19031  efgrelexlemb  19725  efgredeu  19727  imasrng  20158  imasring  20310  znf1o  21531  zzngim  21532  indlcim  21820  1stcfb  23410  upxp  23588  uptx  23590  cnmpt1st  23633  cnmpt2nd  23634  qtoptopon  23669  qtopcld  23678  qtopeu  23681  qtoprest  23682  imastopn  23685  qtophmeo  23782  elfm3  23915  uniiccdif  25545  dirith  27492  nosupno  27667  nosupbday  27669  noinfno  27682  noinfbday  27684  noetasuplem4  27700  noetainflem4  27704  bdayfn  27741  grporn  30592  0vfval  30677  foresf1o  32574  2ndimaxp  32719  2ndresdju  32722  xppreima2  32724  1stpreimas  32779  1stpreima  32780  2ndpreima  32781  fsuppcurry1  32797  fsuppcurry2  32798  ffsrn  32801  gsummpt2d  33110  qusker  33409  imaslmod  33413  qtopt1  33979  qtophaus  33980  circcn  33982  cnre2csqima  34055  sigapildsys  34306  carsgclctunlem3  34464  fnbigcup  36081  filnetlem4  36563  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  ssnnf1octb  45624  nnfoctbdj  46884  fcoreslem4  47514  fcoresf1  47517  fargshiftfo  47902  fonex  49342