Theorem fofn 6798

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 6535  –onto→wfo 6538

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 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ss 3923  df-f 6544  df-fo 6546

This theorem is used by:  fodmrnu  6804  foun  6843  fo00  6861  foelcdmi  6946  cbvfo  7293  foeqcnvco  7304  canth  7370  br1steqg  8010  br2ndeqg  8011  1stcof  8018  2ndcof  8019  df1st2  8095  df2nd2  8096  1stconst  8097  2ndconst  8098  fsplit  8114  smoiso2  8358  fodomfi  9275  brwdom2  9538  fodomfi2  10056  fpwwe  10642  imasaddfnlem  17599  imasvscafn  17608  imasleval  17612  dmaf  18123  cdaf  18124  imasmnd2  18855  imasgrp2  19144  efgrelexlemb  19843  efgredeu  19845  imasrng  20278  imasring  20437  znf1o  21730  zzngim  21731  indlcim  22019  1stcfb  23631  upxp  23809  uptx  23811  cnmpt1st  23854  cnmpt2nd  23855  qtoptopon  23890  qtopcld  23899  qtopeu  23902  qtoprest  23903  imastopn  23906  qtophmeo  24003  elfm3  24136  uniiccdif  25766  dirith  27722  nosupno  27896  nosupbday  27898  noinfno  27911  noinfbday  27913  noetasuplem4  27929  noetainflem4  27933  bdayfn  27970  grporn  30902  0vfval  30987  foresf1o  32879  2ndimaxp  33020  2ndresdju  33023  xppreima2  33025  1stpreimas  33080  1stpreima  33081  2ndpreima  33082  fsuppcurry1  33098  fsuppcurry2  33099  ffsrn  33102  gsummpt2d  33392  qusker  33692  imaslmod  33696  qtopt1  34248  qtophaus  34249  circcn  34251  cnre2csqima  34324  sigapildsys  34576  carsgclctunlem3  34734  rankfn  35523  onvfowev  35616  fnbigcup  36404  filnetlem4  36925  ovoliunnfl  38346  voliunnfl  38348  volsupnfl  38349  ssnnf1octb  45945  nnfoctbdj  47203  fcoreslem4  47836  fcoresf1  47839  fargshiftfo  48224  fonex  49678