Theorem fofn 5511

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 5509	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
2		ffn 5434	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3	1, 2	syl 14	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 5274  ⟶wf 5275  –onto→wfo 5277

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 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3176  df-ss 3183  df-f 5283  df-fo 5285

This theorem is referenced by:  fodmrnu  5517  foun  5552  fo00  5570  foelcdmi  5643  foima2  5832  cbvfo  5866  cbvexfo  5867  foeqcnvco  5871  canth  5909  1stcof  6261  2ndcof  6262  1stexg  6265  2ndexg  6266  df1st2  6317  df2nd2  6318  1stconst  6319  2ndconst  6320  fidcenumlemrks  7069  fidcenumlemr  7071  ctm  7225  suplocexprlemell  7841  ennnfonelemhf1o  12854  ennnfonelemrn  12860  imasaddfnlemg  13216  imasmnd2  13354  imasgrp2  13516  imasrng  13788  imasring  13896  znf1o  14483  upxp  14814  uptx  14816  cnmpt1st  14830  cnmpt2nd  14831  pw1nct  16075