Theorem fofn 6775

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

Syntax hints:   → wi 4   Fn wfn 6511  –onto→wfo 6514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3919  df-f 6520  df-fo 6522

This theorem is referenced by:  fodmrnu  6781  foun  6820  fo00  6838  foelcdmi  6923  cbvfo  7268  foeqcnvco  7279  canth  7345  br1steqg  7987  br2ndeqg  7988  1stcof  7995  2ndcof  7996  df1st2  8071  df2nd2  8072  1stconst  8073  2ndconst  8074  fsplit  8090  smoiso2  8334  fodomfi  9250  brwdom2  9515  fodomfi2  10010  fpwwe  10598  imasaddfnlem  17549  imasvscafn  17558  imasleval  17562  dmaf  18073  cdaf  18074  imasmnd2  18799  imasgrp2  19088  efgrelexlemb  19781  efgredeu  19783  imasrng  20214  imasring  20366  znf1o  21591  zzngim  21592  indlcim  21880  1stcfb  23493  upxp  23671  uptx  23673  cnmpt1st  23716  cnmpt2nd  23717  qtoptopon  23752  qtopcld  23761  qtopeu  23764  qtoprest  23765  imastopn  23768  qtophmeo  23865  elfm3  23998  uniiccdif  25628  dirith  27581  nosupno  27755  nosupbday  27757  noinfno  27770  noinfbday  27772  noetasuplem4  27788  noetainflem4  27792  bdayfn  27829  grporn  30681  0vfval  30766  foresf1o  32663  2ndimaxp  32809  2ndresdju  32812  xppreima2  32814  1stpreimas  32869  1stpreima  32870  2ndpreima  32871  fsuppcurry1  32887  fsuppcurry2  32888  ffsrn  32891  gsummpt2d  33190  qusker  33496  imaslmod  33500  qtopt1  34093  qtophaus  34094  circcn  34096  cnre2csqima  34169  sigapildsys  34420  carsgclctunlem3  34578  onvfowev  35420  fnbigcup  36210  filnetlem4  36702  ovoliunnfl  38122  voliunnfl  38124  volsupnfl  38125  ssnnf1octb  45733  nnfoctbdj  46991  fcoreslem4  47621  fcoresf1  47624  fargshiftfo  48009  fonex  49449