Theorem fofn 5437

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 5435	. 2 |- ( F : A -onto-> B -> F : A --> B )
2		ffn 5362	. 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 5208   -->wf 5209   -onto->wfo 5211

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142  df-f 5217  df-fo 5219

This theorem is referenced by:  fodmrnu  5443  foun  5477  fo00  5494  foelcdmi  5565  foima2  5748  cbvfo  5781  cbvexfo  5782  foeqcnvco  5786  canth  5824  1stcof  6159  2ndcof  6160  1stexg  6163  2ndexg  6164  df1st2  6215  df2nd2  6216  1stconst  6217  2ndconst  6218  fidcenumlemrks  6947  fidcenumlemr  6949  ctm  7103  suplocexprlemell  7707  ennnfonelemhf1o  12404  ennnfonelemrn  12410  upxp  13554  uptx  13556  cnmpt1st  13570  cnmpt2nd  13571  pw1nct  14523