Theorem fofn 6822

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

Syntax hints:   → wi 4   Fn wfn 6557  –onto→wfo 6560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979  df-f 6566  df-fo 6568

This theorem is referenced by:  fodmrnu  6828  foun  6866  fo00  6884  foelcdmi  6969  cbvfo  7308  foeqcnvco  7319  canth  7384  br1steqg  8034  br2ndeqg  8035  1stcof  8042  2ndcof  8043  df1st2  8121  df2nd2  8122  1stconst  8123  2ndconst  8124  fsplit  8140  smoiso2  8407  fodomfi  9347  fodomfiOLD  9367  brwdom2  9610  fodomfi2  10097  fpwwe  10683  imasaddfnlem  17574  imasvscafn  17583  imasleval  17587  dmaf  18102  cdaf  18103  imasmnd2  18799  imasgrp2  19085  efgrelexlemb  19782  efgredeu  19784  imasrng  20194  imasring  20343  znf1o  21587  zzngim  21588  indlcim  21877  1stcfb  23468  upxp  23646  uptx  23648  cnmpt1st  23691  cnmpt2nd  23692  qtoptopon  23727  qtopcld  23736  qtopeu  23739  qtoprest  23740  imastopn  23743  qtophmeo  23840  elfm3  23973  uniiccdif  25626  dirith  27587  nosupno  27762  nosupbday  27764  noinfno  27777  noinfbday  27779  noetasuplem4  27795  noetainflem4  27799  bdayfn  27832  grporn  30549  0vfval  30634  foresf1o  32531  2ndimaxp  32662  2ndresdju  32665  xppreima2  32667  1stpreimas  32720  1stpreima  32721  2ndpreima  32722  fsuppcurry1  32742  fsuppcurry2  32743  ffsrn  32746  gsummpt2d  33034  qusker  33356  imaslmod  33360  qtopt1  33795  qtophaus  33796  circcn  33798  cnre2csqima  33871  sigapildsys  34142  carsgclctunlem3  34301  fnbigcup  35882  filnetlem4  36363  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  ssnnf1octb  45136  nnfoctbdj  46411  fcoreslem4  47015  fcoresf1  47018  fargshiftfo  47366