Theorem fofn 6822

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 6820	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
2	1	ffnd 6737	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 6556  –onto→wfo 6559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968  df-f 6565  df-fo 6567

This theorem is referenced by:  fodmrnu  6828  foun  6866  fo00  6884  foelcdmi  6970  cbvfo  7309  foeqcnvco  7320  canth  7385  br1steqg  8036  br2ndeqg  8037  1stcof  8044  2ndcof  8045  df1st2  8123  df2nd2  8124  1stconst  8125  2ndconst  8126  fsplit  8142  smoiso2  8409  fodomfi  9350  fodomfiOLD  9370  brwdom2  9613  fodomfi2  10100  fpwwe  10686  imasaddfnlem  17573  imasvscafn  17582  imasleval  17586  dmaf  18094  cdaf  18095  imasmnd2  18787  imasgrp2  19073  efgrelexlemb  19768  efgredeu  19770  imasrng  20174  imasring  20327  znf1o  21570  zzngim  21571  indlcim  21860  1stcfb  23453  upxp  23631  uptx  23633  cnmpt1st  23676  cnmpt2nd  23677  qtoptopon  23712  qtopcld  23721  qtopeu  23724  qtoprest  23725  imastopn  23728  qtophmeo  23825  elfm3  23958  uniiccdif  25613  dirith  27573  nosupno  27748  nosupbday  27750  noinfno  27763  noinfbday  27765  noetasuplem4  27781  noetainflem4  27785  bdayfn  27818  grporn  30540  0vfval  30625  foresf1o  32523  2ndimaxp  32656  2ndresdju  32659  xppreima2  32661  1stpreimas  32715  1stpreima  32716  2ndpreima  32717  fsuppcurry1  32736  fsuppcurry2  32737  ffsrn  32740  gsummpt2d  33052  qusker  33377  imaslmod  33381  qtopt1  33834  qtophaus  33835  circcn  33837  cnre2csqima  33910  sigapildsys  34163  carsgclctunlem3  34322  fnbigcup  35902  filnetlem4  36382  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  ssnnf1octb  45199  nnfoctbdj  46471  fcoreslem4  47078  fcoresf1  47081  fargshiftfo  47429