Theorem fofn 6748

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

Syntax hints:   → wi 4   Fn wfn 6487  –onto→wfo 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918  df-f 6496  df-fo 6498

This theorem is referenced by:  fodmrnu  6754  foun  6792  fo00  6810  foelcdmi  6895  cbvfo  7235  foeqcnvco  7246  canth  7312  br1steqg  7955  br2ndeqg  7956  1stcof  7963  2ndcof  7964  df1st2  8040  df2nd2  8041  1stconst  8042  2ndconst  8043  fsplit  8059  smoiso2  8301  fodomfi  9212  fodomfiOLD  9230  brwdom2  9478  fodomfi2  9970  fpwwe  10557  imasaddfnlem  17449  imasvscafn  17458  imasleval  17462  dmaf  17973  cdaf  17974  imasmnd2  18699  imasgrp2  18985  efgrelexlemb  19679  efgredeu  19681  imasrng  20112  imasring  20266  znf1o  21506  zzngim  21507  indlcim  21795  1stcfb  23389  upxp  23567  uptx  23569  cnmpt1st  23612  cnmpt2nd  23613  qtoptopon  23648  qtopcld  23657  qtopeu  23660  qtoprest  23661  imastopn  23664  qtophmeo  23761  elfm3  23894  uniiccdif  25535  dirith  27496  nosupno  27671  nosupbday  27673  noinfno  27686  noinfbday  27688  noetasuplem4  27704  noetainflem4  27708  bdayfn  27745  grporn  30596  0vfval  30681  foresf1o  32579  2ndimaxp  32724  2ndresdju  32727  xppreima2  32729  1stpreimas  32785  1stpreima  32786  2ndpreima  32787  fsuppcurry1  32803  fsuppcurry2  32804  ffsrn  32807  gsummpt2d  33132  qusker  33430  imaslmod  33434  qtopt1  33992  qtophaus  33993  circcn  33995  cnre2csqima  34068  sigapildsys  34319  carsgclctunlem3  34477  fnbigcup  36093  filnetlem4  36575  ovoliunnfl  37863  voliunnfl  37865  volsupnfl  37866  ssnnf1octb  45438  nnfoctbdj  46700  fcoreslem4  47312  fcoresf1  47315  fargshiftfo  47688  fonex  49112