Theorem fofn 6745

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

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

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915  df-f 6493  df-fo 6495

This theorem is referenced by:  fodmrnu  6751  foun  6789  fo00  6807  foelcdmi  6892  cbvfo  7232  foeqcnvco  7243  canth  7309  br1steqg  7952  br2ndeqg  7953  1stcof  7960  2ndcof  7961  df1st2  8037  df2nd2  8038  1stconst  8039  2ndconst  8040  fsplit  8056  smoiso2  8298  fodomfi  9207  fodomfiOLD  9225  brwdom2  9470  fodomfi2  9962  fpwwe  10548  imasaddfnlem  17440  imasvscafn  17449  imasleval  17453  dmaf  17964  cdaf  17965  imasmnd2  18690  imasgrp2  18976  efgrelexlemb  19670  efgredeu  19672  imasrng  20103  imasring  20257  znf1o  21497  zzngim  21498  indlcim  21786  1stcfb  23380  upxp  23558  uptx  23560  cnmpt1st  23603  cnmpt2nd  23604  qtoptopon  23639  qtopcld  23648  qtopeu  23651  qtoprest  23652  imastopn  23655  qtophmeo  23752  elfm3  23885  uniiccdif  25526  dirith  27487  nosupno  27662  nosupbday  27664  noinfno  27677  noinfbday  27679  noetasuplem4  27695  noetainflem4  27699  bdayfn  27732  grporn  30522  0vfval  30607  foresf1o  32505  2ndimaxp  32650  2ndresdju  32653  xppreima2  32655  1stpreimas  32711  1stpreima  32712  2ndpreima  32713  fsuppcurry1  32731  fsuppcurry2  32732  ffsrn  32735  gsummpt2d  33060  qusker  33358  imaslmod  33362  qtopt1  33920  qtophaus  33921  circcn  33923  cnre2csqima  33996  sigapildsys  34247  carsgclctunlem3  34405  fnbigcup  36015  filnetlem4  36497  ovoliunnfl  37775  voliunnfl  37777  volsupnfl  37778  ssnnf1octb  45354  nnfoctbdj  46616  fcoreslem4  47228  fcoresf1  47231  fargshiftfo  47604  fonex  49028