Theorem fofn 5522

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 5520	. 2 |- ( F : A -onto-> B -> F : A --> B )
2		ffn 5445	. 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 5285   -->wf 5286   -onto->wfo 5288

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187  df-f 5294  df-fo 5296

This theorem is referenced by:  fodmrnu  5528  foun  5563  fo00  5581  foelcdmi  5654  foima2  5843  cbvfo  5877  cbvexfo  5878  foeqcnvco  5882  canth  5920  1stcof  6272  2ndcof  6273  1stexg  6276  2ndexg  6277  df1st2  6328  df2nd2  6329  1stconst  6330  2ndconst  6331  fidcenumlemrks  7081  fidcenumlemr  7083  ctm  7237  suplocexprlemell  7861  ennnfonelemhf1o  12899  ennnfonelemrn  12905  imasaddfnlemg  13261  imasmnd2  13399  imasgrp2  13561  imasrng  13833  imasring  13941  znf1o  14528  upxp  14859  uptx  14861  cnmpt1st  14875  cnmpt2nd  14876  pw1nct  16142