Theorem fofn 6748

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

Syntax hints:   → wi 4   Fn wfn 6487  –onto→wfo 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907  df-f 6496  df-fo 6498

This theorem is referenced by:  fodmrnu  6754  foun  6792  fo00  6810  foelcdmi  6895  cbvfo  7237  foeqcnvco  7248  canth  7314  br1steqg  7957  br2ndeqg  7958  1stcof  7965  2ndcof  7966  df1st2  8041  df2nd2  8042  1stconst  8043  2ndconst  8044  fsplit  8060  smoiso2  8302  fodomfi  9215  fodomfiOLD  9233  brwdom2  9481  fodomfi2  9973  fpwwe  10560  imasaddfnlem  17483  imasvscafn  17492  imasleval  17496  dmaf  18007  cdaf  18008  imasmnd2  18733  imasgrp2  19022  efgrelexlemb  19716  efgredeu  19718  imasrng  20149  imasring  20301  znf1o  21541  zzngim  21542  indlcim  21830  1stcfb  23420  upxp  23598  uptx  23600  cnmpt1st  23643  cnmpt2nd  23644  qtoptopon  23679  qtopcld  23688  qtopeu  23691  qtoprest  23692  imastopn  23695  qtophmeo  23792  elfm3  23925  uniiccdif  25555  dirith  27506  nosupno  27681  nosupbday  27683  noinfno  27696  noinfbday  27698  noetasuplem4  27714  noetainflem4  27718  bdayfn  27755  grporn  30607  0vfval  30692  foresf1o  32589  2ndimaxp  32734  2ndresdju  32737  xppreima2  32739  1stpreimas  32794  1stpreima  32795  2ndpreima  32796  fsuppcurry1  32812  fsuppcurry2  32813  ffsrn  32816  gsummpt2d  33125  qusker  33424  imaslmod  33428  qtopt1  33995  qtophaus  33996  circcn  33998  cnre2csqima  34071  sigapildsys  34322  carsgclctunlem3  34480  fnbigcup  36097  filnetlem4  36579  ovoliunnfl  37997  voliunnfl  37999  volsupnfl  38000  ssnnf1octb  45642  nnfoctbdj  46902  fcoreslem4  47526  fcoresf1  47529  fargshiftfo  47914  fonex  49354