Theorem fofn 5617

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

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

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 5381  df-fo 5383

This theorem is used by:  fodmrnu  5623  foun  5658  fo00  5677  foelcdmi  5755  foima2  5957  cbvfo  5991  cbvexfo  5992  foeqcnvco  5996  canth  6036  1stcof  6397  2ndcof  6398  1stexg  6401  2ndexg  6402  df1st2  6455  df2nd2  6456  1stconst  6457  2ndconst  6458  fidcenumlemrks  7270  fidcenumlemr  7272  ctm  7449  suplocexprlemell  8080  ennnfonelemhf1o  13304  ennnfonelemrn  13310  imasaddfnlemg  13635  imasmnd2  13759  imasgrp2  13913  imasrng  14255  imasring  14369  znf1o  14986  upxp  15373  uptx  15375  cnmpt1st  15389  cnmpt2nd  15390  pw1nct  17033