Theorem fofn 5615

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 5370  ⟶wf 5371  –onto→wfo 5373

This proof depends on 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 proof 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 5379  df-fo 5381

This theorem is used by:  fodmrnu  5621  foun  5656  fo00  5675  foelcdmi  5752  foima2  5951  cbvfo  5985  cbvexfo  5986  foeqcnvco  5990  canth  6030  1stcof  6391  2ndcof  6392  1stexg  6395  2ndexg  6396  df1st2  6449  df2nd2  6450  1stconst  6451  2ndconst  6452  fidcenumlemrks  7264  fidcenumlemr  7266  ctm  7443  suplocexprlemell  8074  ennnfonelemhf1o  13287  ennnfonelemrn  13293  imasaddfnlemg  13618  imasmnd2  13742  imasgrp2  13896  imasrng  14238  imasring  14352  znf1o  14969  upxp  15356  uptx  15358  cnmpt1st  15372  cnmpt2nd  15373  pw1nct  17016