Theorem fofn 6756

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

Syntax hints:   → wi 4   Fn wfn 6494  –onto→wfo 6497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3928  df-f 6503  df-fo 6505

This theorem is referenced by:  fodmrnu  6762  foun  6800  fo00  6818  foelcdmi  6904  cbvfo  7246  foeqcnvco  7257  canth  7323  br1steqg  7969  br2ndeqg  7970  1stcof  7977  2ndcof  7978  df1st2  8054  df2nd2  8055  1stconst  8056  2ndconst  8057  fsplit  8073  smoiso2  8315  fodomfi  9237  fodomfiOLD  9257  brwdom2  9502  fodomfi2  9989  fpwwe  10575  imasaddfnlem  17467  imasvscafn  17476  imasleval  17480  dmaf  17987  cdaf  17988  imasmnd2  18677  imasgrp2  18963  efgrelexlemb  19656  efgredeu  19658  imasrng  20062  imasring  20215  znf1o  21437  zzngim  21438  indlcim  21725  1stcfb  23308  upxp  23486  uptx  23488  cnmpt1st  23531  cnmpt2nd  23532  qtoptopon  23567  qtopcld  23576  qtopeu  23579  qtoprest  23580  imastopn  23583  qtophmeo  23680  elfm3  23813  uniiccdif  25455  dirith  27416  nosupno  27591  nosupbday  27593  noinfno  27606  noinfbday  27608  noetasuplem4  27624  noetainflem4  27628  bdayfn  27661  grporn  30423  0vfval  30508  foresf1o  32406  2ndimaxp  32543  2ndresdju  32546  xppreima2  32548  1stpreimas  32602  1stpreima  32603  2ndpreima  32604  fsuppcurry1  32621  fsuppcurry2  32622  ffsrn  32625  gsummpt2d  32962  qusker  33293  imaslmod  33297  qtopt1  33798  qtophaus  33799  circcn  33801  cnre2csqima  33874  sigapildsys  34125  carsgclctunlem3  34284  fnbigcup  35862  filnetlem4  36342  ovoliunnfl  37629  voliunnfl  37631  volsupnfl  37632  ssnnf1octb  45161  nnfoctbdj  46427  fcoreslem4  47040  fcoresf1  47043  fargshiftfo  47416  fonex  48828