Theorem fofn 5432

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 5430	. 2 |- ( F : A -onto-> B -> F : A --> B )
2		ffn 5357	. 2 |- ( F : A --> B -> F Fn A )
3	1, 2	syl 14	1 |- ( F : A -onto-> B -> F Fn A )

Syntax hints:   -> wi 4   Fn wfn 5203   -->wf 5204   -onto->wfo 5206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-11 1504  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-in 3133  df-ss 3140  df-f 5212  df-fo 5214

This theorem is referenced by:  fodmrnu  5438  foun  5472  fo00  5489  foelcdmi  5560  foima2  5743  cbvfo  5776  cbvexfo  5777  foeqcnvco  5781  canth  5819  1stcof  6154  2ndcof  6155  1stexg  6158  2ndexg  6159  df1st2  6210  df2nd2  6211  1stconst  6212  2ndconst  6213  fidcenumlemrks  6942  fidcenumlemr  6944  ctm  7098  suplocexprlemell  7687  ennnfonelemhf1o  12379  ennnfonelemrn  12385  upxp  13341  uptx  13343  cnmpt1st  13357  cnmpt2nd  13358  pw1nct  14311