Theorem fofn 6836

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

Syntax hints:   → wi 4   Fn wfn 6568  –onto→wfo 6571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993  df-f 6577  df-fo 6579

This theorem is referenced by:  fodmrnu  6842  foun  6880  fo00  6898  foelcdmi  6983  cbvfo  7325  foeqcnvco  7336  canth  7401  br1steqg  8052  br2ndeqg  8053  1stcof  8060  2ndcof  8061  df1st2  8139  df2nd2  8140  1stconst  8141  2ndconst  8142  fsplit  8158  smoiso2  8425  fodomfi  9378  fodomfiOLD  9398  brwdom2  9642  fodomfi2  10129  fpwwe  10715  imasaddfnlem  17588  imasvscafn  17597  imasleval  17601  dmaf  18116  cdaf  18117  imasmnd2  18809  imasgrp2  19095  efgrelexlemb  19792  efgredeu  19794  imasrng  20204  imasring  20353  znf1o  21593  zzngim  21594  indlcim  21883  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  25632  dirith  27591  nosupno  27766  nosupbday  27768  noinfno  27781  noinfbday  27783  noetasuplem4  27799  noetainflem4  27803  bdayfn  27836  grporn  30553  0vfval  30638  foresf1o  32532  2ndimaxp  32665  2ndresdju  32667  xppreima2  32669  1stpreimas  32717  1stpreima  32718  2ndpreima  32719  fsuppcurry1  32739  fsuppcurry2  32740  ffsrn  32743  gsummpt2d  33032  qusker  33342  imaslmod  33346  qtopt1  33781  qtophaus  33782  circcn  33784  cnre2csqima  33857  sigapildsys  34126  carsgclctunlem3  34285  fnbigcup  35865  filnetlem4  36347  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  ssnnf1octb  45101  nnfoctbdj  46377  fcoreslem4  46981  fcoresf1  46984  fargshiftfo  47316