Theorem fofn 6117

Description: An onto mapping is a function on its domain. (Contributed by NM, 16-Dec-2008.)

Assertion

Ref	Expression
fofn	|- ( F : A -onto-> B -> F Fn A )

Proof of Theorem fofn

Step	Hyp	Ref	Expression
1		fof 6115	. 2 |- ( F : A -onto-> B -> F : A --> B )
2	1	ffnd 6046	1 |- ( F : A -onto-> B -> F Fn A )

Syntax hints:   -> wi 4   Fn wfn 5883   -onto->wfo 5886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588  df-f 5892  df-fo 5894

This theorem is referenced by:  fodmrnu  6123  foun  6155  fo00  6172  foelrni  6244  cbvfo  6544  foeqcnvco  6555  canth  6608  1stcof  7196  2ndcof  7197  df1st2  7263  df2nd2  7264  1stconst  7265  2ndconst  7266  fsplit  7282  smoiso2  7466  fodomfi  8239  brwdom2  8478  fodomfi2  8883  fpwwe  9468  imasaddfnlem  16188  imasvscafn  16197  imasleval  16201  dmaf  16699  cdaf  16700  imasmnd2  17327  imasgrp2  17530  efgrelexlemb  18163  efgredeu  18165  imasring  18619  znf1o  19900  zzngim  19901  indlcim  20179  1stcfb  21248  upxp  21426  uptx  21428  cnmpt1st  21471  cnmpt2nd  21472  qtoptopon  21507  qtopcld  21516  qtopeu  21519  qtoprest  21520  imastopn  21523  qtophmeo  21620  elfm3  21754  uniiccdif  23346  dirith  25218  grporn  27375  0vfval  27461  foresf1o  29343  xppreima2  29450  1stpreimas  29483  1stpreima  29484  2ndpreima  29485  ffsrn  29504  gsummpt2d  29781  qtopt1  29902  qtophaus  29903  circcn  29905  cnre2csqima  29957  sigapildsys  30225  carsgclctunlem3  30382  br1steq  31670  br2ndeq  31671  br1steqg  31672  br2ndeqg  31673  nosupno  31849  nosupbday  31851  noetalem3  31865  bdayfn  31889  fnbigcup  32008  filnetlem4  32376  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  ssnnf1octb  39382  nnfoctbdj  40673  fargshiftfo  41378