Theorem fofn 6765

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

Syntax hints:   → wi 4   Fn wfn 6501  –onto→wfo 6504

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-cleq 2744  df-ss 3912  df-f 6510  df-fo 6512

This theorem is referenced by:  fodmrnu  6771  foun  6810  fo00  6828  foelcdmi  6913  cbvfo  7258  foeqcnvco  7269  canth  7335  br1steqg  7977  br2ndeqg  7978  1stcof  7985  2ndcof  7986  df1st2  8061  df2nd2  8062  1stconst  8063  2ndconst  8064  fsplit  8080  smoiso2  8324  fodomfi  9241  fodomfiOLD  9259  brwdom2  9507  fodomfi2  10002  fpwwe  10590  imasaddfnlem  17530  imasvscafn  17539  imasleval  17543  dmaf  18054  cdaf  18055  imasmnd2  18780  imasgrp2  19069  efgrelexlemb  19762  efgredeu  19764  imasrng  20195  imasring  20347  znf1o  21572  zzngim  21573  indlcim  21861  1stcfb  23474  upxp  23652  uptx  23654  cnmpt1st  23697  cnmpt2nd  23698  qtoptopon  23733  qtopcld  23742  qtopeu  23745  qtoprest  23746  imastopn  23749  qtophmeo  23846  elfm3  23979  uniiccdif  25609  dirith  27559  nosupno  27733  nosupbday  27735  noinfno  27748  noinfbday  27750  noetasuplem4  27766  noetainflem4  27770  bdayfn  27807  grporn  30659  0vfval  30744  foresf1o  32641  2ndimaxp  32787  2ndresdju  32790  xppreima2  32792  1stpreimas  32847  1stpreima  32848  2ndpreima  32849  fsuppcurry1  32865  fsuppcurry2  32866  ffsrn  32869  gsummpt2d  33179  qusker  33481  imaslmod  33485  qtopt1  34076  qtophaus  34077  circcn  34079  cnre2csqima  34152  sigapildsys  34403  carsgclctunlem3  34561  fnbigcup  36187  filnetlem4  36679  ovoliunnfl  38099  voliunnfl  38101  volsupnfl  38102  ssnnf1octb  45710  nnfoctbdj  46968  fcoreslem4  47598  fcoresf1  47601  fargshiftfo  47986  fonex  49426