Theorem fofn 5422

Description: An onto mapping is a function on its domain. (Contributed by NM, 16-Dec-2008.)

Assertion

Ref	Expression
fofn	⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴)

Proof of Theorem fofn

Step	Hyp	Ref	Expression
1		fof 5420	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
2		ffn 5347	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3	1, 2	syl 14	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 5193  ⟶wf 5194  –onto→wfo 5196

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134  df-f 5202  df-fo 5204

This theorem is referenced by:  fodmrnu  5428  foun  5461  fo00  5478  foima2  5731  cbvfo  5764  cbvexfo  5765  foeqcnvco  5769  canth  5807  1stcof  6142  2ndcof  6143  1stexg  6146  2ndexg  6147  df1st2  6198  df2nd2  6199  1stconst  6200  2ndconst  6201  fidcenumlemrks  6930  fidcenumlemr  6932  ctm  7086  suplocexprlemell  7675  ennnfonelemhf1o  12368  ennnfonelemrn  12374  upxp  13066  uptx  13068  cnmpt1st  13082  cnmpt2nd  13083  pw1nct  14036