Theorem fofn 6690

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

Syntax hints:   → wi 4   Fn wfn 6428  –onto→wfo 6431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-f 6437  df-fo 6439

This theorem is referenced by:  fodmrnu  6696  foun  6734  fo00  6752  foelrni  6831  cbvfo  7161  foeqcnvco  7172  canth  7229  br1steqg  7853  br2ndeqg  7854  1stcof  7861  2ndcof  7862  df1st2  7938  df2nd2  7939  1stconst  7940  2ndconst  7941  fsplit  7957  fsplitOLD  7958  smoiso2  8200  fodomfi  9092  brwdom2  9332  fodomfi2  9816  fpwwe  10402  imasaddfnlem  17239  imasvscafn  17248  imasleval  17252  dmaf  17764  cdaf  17765  imasmnd2  18422  imasgrp2  18690  efgrelexlemb  19356  efgredeu  19358  imasring  19858  znf1o  20759  zzngim  20760  indlcim  21047  1stcfb  22596  upxp  22774  uptx  22776  cnmpt1st  22819  cnmpt2nd  22820  qtoptopon  22855  qtopcld  22864  qtopeu  22867  qtoprest  22868  imastopn  22871  qtophmeo  22968  elfm3  23101  uniiccdif  24742  dirith  26677  grporn  28883  0vfval  28968  foresf1o  30850  2ndimaxp  30984  2ndresdju  30986  xppreima2  30988  1stpreimas  31038  1stpreima  31039  2ndpreima  31040  fsuppcurry1  31060  fsuppcurry2  31061  ffsrn  31064  gsummpt2d  31309  qusker  31549  imaslmod  31553  qtopt1  31785  qtophaus  31786  circcn  31788  cnre2csqima  31861  sigapildsys  32130  carsgclctunlem3  32287  nosupno  33906  nosupbday  33908  noinfno  33921  noinfbday  33923  noetasuplem4  33939  noetainflem4  33943  bdayfn  33968  fnbigcup  34203  filnetlem4  34570  ovoliunnfl  35819  voliunnfl  35821  volsupnfl  35822  ssnnf1octb  42733  nnfoctbdj  43994  fcoreslem4  44560  fcoresf1  44563  fargshiftfo  44894