Theorem fofn 6791

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

Syntax hints:   → wi 4   Fn wfn 6525  –onto→wfo 6528

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 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ss 3943  df-f 6534  df-fo 6536

This theorem is referenced by:  fodmrnu  6797  foun  6835  fo00  6853  foelcdmi  6939  cbvfo  7281  foeqcnvco  7292  canth  7357  br1steqg  8008  br2ndeqg  8009  1stcof  8016  2ndcof  8017  df1st2  8095  df2nd2  8096  1stconst  8097  2ndconst  8098  fsplit  8114  smoiso2  8381  fodomfi  9320  fodomfiOLD  9340  brwdom2  9585  fodomfi2  10072  fpwwe  10658  imasaddfnlem  17540  imasvscafn  17549  imasleval  17553  dmaf  18060  cdaf  18061  imasmnd2  18750  imasgrp2  19036  efgrelexlemb  19729  efgredeu  19731  imasrng  20135  imasring  20288  znf1o  21510  zzngim  21511  indlcim  21798  1stcfb  23381  upxp  23559  uptx  23561  cnmpt1st  23604  cnmpt2nd  23605  qtoptopon  23640  qtopcld  23649  qtopeu  23652  qtoprest  23653  imastopn  23656  qtophmeo  23753  elfm3  23886  uniiccdif  25529  dirith  27490  nosupno  27665  nosupbday  27667  noinfno  27680  noinfbday  27682  noetasuplem4  27698  noetainflem4  27702  bdayfn  27735  grporn  30448  0vfval  30533  foresf1o  32431  2ndimaxp  32570  2ndresdju  32573  xppreima2  32575  1stpreimas  32629  1stpreima  32630  2ndpreima  32631  fsuppcurry1  32648  fsuppcurry2  32649  ffsrn  32652  gsummpt2d  32989  qusker  33310  imaslmod  33314  qtopt1  33812  qtophaus  33813  circcn  33815  cnre2csqima  33888  sigapildsys  34139  carsgclctunlem3  34298  fnbigcup  35865  filnetlem4  36345  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  ssnnf1octb  45166  nnfoctbdj  46433  fcoreslem4  47043  fcoresf1  47046  fargshiftfo  47404  fonex  48790