Theorem fofn 5612

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 5610	. 2 |- ( F : A -onto-> B -> F : A --> B )
2		ffn 5528	. 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 5367   -->wf 5368   -onto->wfo 5370

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233  df-f 5376  df-fo 5378

This theorem is referenced by:  fodmrnu  5618  foun  5653  fo00  5672  foelcdmi  5749  foima2  5947  cbvfo  5981  cbvexfo  5982  foeqcnvco  5986  canth  6026  1stcof  6387  2ndcof  6388  1stexg  6391  2ndexg  6392  df1st2  6445  df2nd2  6446  1stconst  6447  2ndconst  6448  fidcenumlemrks  7260  fidcenumlemr  7262  ctm  7439  suplocexprlemell  8070  ennnfonelemhf1o  13282  ennnfonelemrn  13288  imasaddfnlemg  13612  imasmnd2  13736  imasgrp2  13890  imasrng  14230  imasring  14342  znf1o  14958  upxp  15296  uptx  15298  cnmpt1st  15312  cnmpt2nd  15313  pw1nct  16947