Theorem fofn 5355

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 5353	. 2 |- ( F : A -onto-> B -> F : A --> B )
2		ffn 5280	. 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 5126   -->wf 5127   -onto->wfo 5129

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089  df-f 5135  df-fo 5137

This theorem is referenced by:  fodmrnu  5361  foun  5394  fo00  5411  foima2  5661  cbvfo  5694  cbvexfo  5695  foeqcnvco  5699  1stcof  6069  2ndcof  6070  1stexg  6073  2ndexg  6074  df1st2  6124  df2nd2  6125  1stconst  6126  2ndconst  6127  fidcenumlemrks  6849  fidcenumlemr  6851  ctm  7002  suplocexprlemell  7545  ennnfonelemhf1o  11962  ennnfonelemrn  11968  upxp  12480  uptx  12482  cnmpt1st  12496  cnmpt2nd  12497  pw1nct  13371