Theorem fofn 6567

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

Syntax hints:   → wi 4   Fn wfn 6319  –onto→wfo 6322

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-f 6328  df-fo 6330

This theorem is referenced by:  fodmrnu  6573  foun  6608  fo00  6625  foelrni  6702  cbvfo  7023  foeqcnvco  7034  canth  7090  br1steqg  7693  br2ndeqg  7694  1stcof  7701  2ndcof  7702  df1st2  7776  df2nd2  7777  1stconst  7778  2ndconst  7779  fsplit  7795  fsplitOLD  7796  smoiso2  7989  fodomfi  8781  brwdom2  9021  fodomfi2  9471  fpwwe  10057  imasaddfnlem  16793  imasvscafn  16802  imasleval  16806  dmaf  17301  cdaf  17302  imasmnd2  17940  imasgrp2  18206  efgrelexlemb  18868  efgredeu  18870  imasring  19365  znf1o  20243  zzngim  20244  indlcim  20529  1stcfb  22050  upxp  22228  uptx  22230  cnmpt1st  22273  cnmpt2nd  22274  qtoptopon  22309  qtopcld  22318  qtopeu  22321  qtoprest  22322  imastopn  22325  qtophmeo  22422  elfm3  22555  uniiccdif  24182  dirith  26113  grporn  28304  0vfval  28389  foresf1o  30273  2ndimaxp  30409  2ndresdju  30411  xppreima2  30413  1stpreimas  30465  1stpreima  30466  2ndpreima  30467  fsuppcurry1  30487  fsuppcurry2  30488  ffsrn  30491  gsummpt2d  30734  qusker  30969  imaslmod  30973  qtopt1  31188  qtophaus  31189  circcn  31191  cnre2csqima  31264  sigapildsys  31531  carsgclctunlem3  31688  nosupno  33316  nosupbday  33318  noetalem3  33332  bdayfn  33356  fnbigcup  33475  filnetlem4  33842  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  ssnnf1octb  41822  nnfoctbdj  43095  fargshiftfo  43959