Theorem fofn 6796

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

Syntax hints:   → wi 4   Fn wfn 6533  –onto→wfo 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923  df-f 6542  df-fo 6544

This theorem is referenced by:  fodmrnu  6802  foun  6841  fo00  6859  foelcdmi  6944  cbvfo  7289  foeqcnvco  7300  canth  7366  br1steqg  8009  br2ndeqg  8010  1stcof  8017  2ndcof  8018  df1st2  8094  df2nd2  8095  1stconst  8096  2ndconst  8097  fsplit  8113  smoiso2  8357  fodomfi  9273  brwdom2  9536  fodomfi2  10045  fpwwe  10632  imasaddfnlem  17583  imasvscafn  17592  imasleval  17596  dmaf  18107  cdaf  18108  imasmnd2  18833  imasgrp2  19122  efgrelexlemb  19821  efgredeu  19823  imasrng  20256  imasring  20413  znf1o  21682  zzngim  21683  indlcim  21971  1stcfb  23583  upxp  23761  uptx  23763  cnmpt1st  23806  cnmpt2nd  23807  qtoptopon  23842  qtopcld  23851  qtopeu  23854  qtoprest  23855  imastopn  23858  qtophmeo  23955  elfm3  24088  uniiccdif  25718  dirith  27674  nosupno  27848  nosupbday  27850  noinfno  27863  noinfbday  27865  noetasuplem4  27881  noetainflem4  27885  bdayfn  27922  grporn  30854  0vfval  30939  foresf1o  32831  2ndimaxp  32972  2ndresdju  32975  xppreima2  32977  1stpreimas  33032  1stpreima  33033  2ndpreima  33034  fsuppcurry1  33050  fsuppcurry2  33051  ffsrn  33054  gsummpt2d  33350  qusker  33650  imaslmod  33654  qtopt1  34206  qtophaus  34207  circcn  34209  cnre2csqima  34282  sigapildsys  34533  carsgclctunlem3  34691  rankfn  35487  onvfowev  35581  fnbigcup  36372  filnetlem4  36873  ovoliunnfl  38294  voliunnfl  38296  volsupnfl  38297  ssnnf1octb  45895  nnfoctbdj  47153  fcoreslem4  47786  fcoresf1  47789  fargshiftfo  48174  fonex  49628