Theorem fofn 6828

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 6561  ⟶ontowfo 6564

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901  df-f 6570  df-fo 6572

This theorem is used by:  fodmrnu  6834  foun  6873  fo00  6892  foelcdmi  6977  cbvfo  7328  foeqcnvco  7339  canth  7405  br1steqg  8057  br2ndeqg  8058  1stcof  8065  2ndcof  8066  df1st2  8146  df2nd2  8147  1stconst  8148  2ndconst  8149  fsplit  8165  smoiso2  8415  fodomfi  9342  brwdom2  9604  fodomfi2  10178  fpwwe  10770  imasaddfnlem  17750  imasvscafn  17759  imasleval  17763  dmaf  18274  cdaf  18275  imasmgm2  18913  imasmnd2  19018  imasgrp2  19315  efgrelexlemb  20015  efgredeu  20017  imasrng  20450  imasring  20611  znf1o  21912  zzngim  21913  indlcim  22201  1stcfb  23818  upxp  23997  uptx  23999  cnmpt1st  24042  cnmpt2nd  24043  qtoptopon  24078  qtopcld  24087  qtopeu  24090  qtoprest  24091  imastopn  24094  qtophmeo  24191  elfm3  24324  uniiccdif  25954  dirith  27913  nosupno  28117  nosupbday  28119  noinfno  28132  noinfbday  28134  noetasuplem4  28150  noetainflem4  28154  bdayfn  28191  grporn  31180  0vfval  31265  foresf1o  33199  2ndimaxp  33338  2ndresdju  33341  xppreima2  33343  1stpreimas  33396  1stpreima  33397  2ndpreima  33398  fsuppcurry1  33412  fsuppcurry2  33413  ffsrn  33416  gsummpt2d  33709  qusker  34014  imaslmod  34018  qtopt1  34578  qtophaus  34579  circcn  34581  cnre2csqima  34654  sigapildsys  34906  carsgclctunlem3  35063  rankfn  35859  onvfowev  36091  fnbigcup  36878  filnetlem4  37384  ovoliunnfl  38848  voliunnfl  38850  volsupnfl  38851  ssnnf1octb  46482  nnfoctbdj  47739  fcoreslem4  48409  fcoresf1  48412  fargshiftfo  48797  fonex  50309