Theorem fofn 6791

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 6528  –onto→wfo 6531

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ss 3916  df-f 6537  df-fo 6539

This theorem is used by:  fodmrnu  6797  foun  6836  fo00  6854  foelcdmi  6939  cbvfo  7290  foeqcnvco  7301  canth  7367  br1steqg  8008  br2ndeqg  8009  1stcof  8016  2ndcof  8017  df1st2  8095  df2nd2  8096  1stconst  8097  2ndconst  8098  fsplit  8114  smoiso2  8358  fodomfi  9282  brwdom2  9545  fodomfi2  10063  fpwwe  10655  imasaddfnlem  17614  imasvscafn  17623  imasleval  17627  dmaf  18138  cdaf  18139  imasmgm2  18776  imasmnd2  18881  imasgrp2  19178  efgrelexlemb  19877  efgredeu  19879  imasrng  20312  imasring  20471  znf1o  21764  zzngim  21765  indlcim  22053  1stcfb  23670  upxp  23849  uptx  23851  cnmpt1st  23894  cnmpt2nd  23895  qtoptopon  23930  qtopcld  23939  qtopeu  23942  qtoprest  23943  imastopn  23946  qtophmeo  24043  elfm3  24176  uniiccdif  25806  dirith  27765  nosupno  27939  nosupbday  27941  noinfno  27954  noinfbday  27956  noetasuplem4  27972  noetainflem4  27976  bdayfn  28013  grporn  31002  0vfval  31087  foresf1o  32979  2ndimaxp  33119  2ndresdju  33122  xppreima2  33124  1stpreimas  33178  1stpreima  33179  2ndpreima  33180  fsuppcurry1  33195  fsuppcurry2  33196  ffsrn  33199  gsummpt2d  33489  qusker  33789  imaslmod  33793  qtopt1  34345  qtophaus  34346  circcn  34348  cnre2csqima  34421  sigapildsys  34673  carsgclctunlem3  34831  rankfn  35620  onvfowev  35713  fnbigcup  36478  filnetlem4  37000  ovoliunnfl  38411  voliunnfl  38413  volsupnfl  38414  ssnnf1octb  46026  nnfoctbdj  47284  fcoreslem4  47954  fcoresf1  47957  fargshiftfo  48342  fonex  49795