Theorem fofn 6356

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

Syntax hints:   → wi 4   Fn wfn 6119  –onto→wfo 6122

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2804

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-in 3806  df-ss 3813  df-f 6128  df-fo 6130

This theorem is referenced by:  fodmrnu  6362  foun  6397  fo00  6414  foelrni  6492  cbvfo  6800  foeqcnvco  6811  canth  6864  br1steqg  7451  br2ndeqg  7452  1stcof  7459  2ndcof  7460  df1st2  7528  df2nd2  7529  1stconst  7530  2ndconst  7531  fsplit  7547  smoiso2  7733  fodomfi  8509  brwdom2  8748  fodomfi2  9197  fpwwe  9784  imasaddfnlem  16542  imasvscafn  16551  imasleval  16555  dmaf  17052  cdaf  17053  imasmnd2  17681  imasgrp2  17885  efgrelexlemb  18517  efgredeu  18519  imasring  18974  znf1o  20260  zzngim  20261  indlcim  20547  1stcfb  21620  upxp  21798  uptx  21800  cnmpt1st  21843  cnmpt2nd  21844  qtoptopon  21879  qtopcld  21888  qtopeu  21891  qtoprest  21892  imastopn  21895  qtophmeo  21992  elfm3  22125  uniiccdif  23745  dirith  25632  grporn  27932  0vfval  28017  foresf1o  29892  xppreima2  30000  1stpreimas  30032  1stpreima  30033  2ndpreima  30034  ffsrn  30053  gsummpt2d  30327  qtopt1  30448  qtophaus  30449  circcn  30451  cnre2csqima  30503  sigapildsys  30771  carsgclctunlem3  30928  nosupno  32389  nosupbday  32391  noetalem3  32405  bdayfn  32429  fnbigcup  32548  filnetlem4  32915  ovoliunnfl  33996  voliunnfl  33998  volsupnfl  33999  ssnnf1octb  40191  nnfoctbdj  41465  fargshiftfo  42267