Theorem fofn 6792

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

Syntax hints:   → wi 4   Fn wfn 6528  –onto→wfo 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930  df-f 6537  df-fo 6539

This theorem is referenced by:  fodmrnu  6798  foun  6837  fo00  6855  foelcdmi  6940  cbvfo  7285  foeqcnvco  7296  canth  7362  br1steqg  8004  br2ndeqg  8005  1stcof  8012  2ndcof  8013  df1st2  8089  df2nd2  8090  1stconst  8091  2ndconst  8092  fsplit  8108  smoiso2  8352  fodomfi  9268  brwdom2  9531  fodomfi2  10040  fpwwe  10627  imasaddfnlem  17578  imasvscafn  17587  imasleval  17591  dmaf  18102  cdaf  18103  imasmnd2  18828  imasgrp2  19117  efgrelexlemb  19816  efgredeu  19818  imasrng  20251  imasring  20408  znf1o  21666  zzngim  21667  indlcim  21955  1stcfb  23567  upxp  23745  uptx  23747  cnmpt1st  23790  cnmpt2nd  23791  qtoptopon  23826  qtopcld  23835  qtopeu  23838  qtoprest  23839  imastopn  23842  qtophmeo  23939  elfm3  24072  uniiccdif  25702  dirith  27655  nosupno  27829  nosupbday  27831  noinfno  27844  noinfbday  27846  noetasuplem4  27862  noetainflem4  27866  bdayfn  27903  grporn  30810  0vfval  30895  foresf1o  32787  2ndimaxp  32928  2ndresdju  32931  xppreima2  32933  1stpreimas  32988  1stpreima  32989  2ndpreima  32990  fsuppcurry1  33006  fsuppcurry2  33007  ffsrn  33010  gsummpt2d  33306  qusker  33608  imaslmod  33612  qtopt1  34166  qtophaus  34167  circcn  34169  cnre2csqima  34242  sigapildsys  34493  carsgclctunlem3  34651  onvfowev  35495  fnbigcup  36286  filnetlem4  36777  ovoliunnfl  38196  voliunnfl  38198  volsupnfl  38199  ssnnf1octb  45797  nnfoctbdj  47055  fcoreslem4  47685  fcoresf1  47688  fargshiftfo  48073  fonex  49523