Theorem fofn 6807

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

Syntax hints:   → wi 4   Fn wfn 6537  –onto→wfo 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-in 3951  df-ss 3961  df-f 6546  df-fo 6548

This theorem is referenced by:  fodmrnu  6813  foun  6851  fo00  6869  foelcdmi  6954  cbvfo  7292  foeqcnvco  7303  canth  7367  br1steqg  8009  br2ndeqg  8010  1stcof  8017  2ndcof  8018  df1st2  8097  df2nd2  8098  1stconst  8099  2ndconst  8100  fsplit  8116  smoiso2  8383  fodomfi  9341  brwdom2  9588  fodomfi2  10075  fpwwe  10661  imasaddfnlem  17501  imasvscafn  17510  imasleval  17514  dmaf  18029  cdaf  18030  imasmnd2  18722  imasgrp2  19002  efgrelexlemb  19696  efgredeu  19698  imasrng  20108  imasring  20255  znf1o  21472  zzngim  21473  indlcim  21761  1stcfb  23336  upxp  23514  uptx  23516  cnmpt1st  23559  cnmpt2nd  23560  qtoptopon  23595  qtopcld  23604  qtopeu  23607  qtoprest  23608  imastopn  23611  qtophmeo  23708  elfm3  23841  uniiccdif  25494  dirith  27449  nosupno  27623  nosupbday  27625  noinfno  27638  noinfbday  27640  noetasuplem4  27656  noetainflem4  27660  bdayfn  27693  grporn  30318  0vfval  30403  foresf1o  32286  2ndimaxp  32416  2ndresdju  32418  xppreima2  32420  1stpreimas  32469  1stpreima  32470  2ndpreima  32471  fsuppcurry1  32491  fsuppcurry2  32492  ffsrn  32495  gsummpt2d  32741  qusker  33001  imaslmod  33005  qtopt1  33372  qtophaus  33373  circcn  33375  cnre2csqima  33448  sigapildsys  33717  carsgclctunlem3  33876  fnbigcup  35433  filnetlem4  35801  ovoliunnfl  37070  voliunnfl  37072  volsupnfl  37073  ssnnf1octb  44490  nnfoctbdj  45767  fcoreslem4  46371  fcoresf1  46374  fargshiftfo  46705