Theorem fofn 6777

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

Syntax hints:   → wi 4   Fn wfn 6509  –onto→wfo 6512

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934  df-f 6518  df-fo 6520

This theorem is referenced by:  fodmrnu  6783  foun  6821  fo00  6839  foelcdmi  6925  cbvfo  7267  foeqcnvco  7278  canth  7344  br1steqg  7993  br2ndeqg  7994  1stcof  8001  2ndcof  8002  df1st2  8080  df2nd2  8081  1stconst  8082  2ndconst  8083  fsplit  8099  smoiso2  8341  fodomfi  9268  fodomfiOLD  9288  brwdom2  9533  fodomfi2  10020  fpwwe  10606  imasaddfnlem  17498  imasvscafn  17507  imasleval  17511  dmaf  18018  cdaf  18019  imasmnd2  18708  imasgrp2  18994  efgrelexlemb  19687  efgredeu  19689  imasrng  20093  imasring  20246  znf1o  21468  zzngim  21469  indlcim  21756  1stcfb  23339  upxp  23517  uptx  23519  cnmpt1st  23562  cnmpt2nd  23563  qtoptopon  23598  qtopcld  23607  qtopeu  23610  qtoprest  23611  imastopn  23614  qtophmeo  23711  elfm3  23844  uniiccdif  25486  dirith  27447  nosupno  27622  nosupbday  27624  noinfno  27637  noinfbday  27639  noetasuplem4  27655  noetainflem4  27659  bdayfn  27692  grporn  30457  0vfval  30542  foresf1o  32440  2ndimaxp  32577  2ndresdju  32580  xppreima2  32582  1stpreimas  32636  1stpreima  32637  2ndpreima  32638  fsuppcurry1  32655  fsuppcurry2  32656  ffsrn  32659  gsummpt2d  32996  qusker  33327  imaslmod  33331  qtopt1  33832  qtophaus  33833  circcn  33835  cnre2csqima  33908  sigapildsys  34159  carsgclctunlem3  34318  fnbigcup  35896  filnetlem4  36376  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  ssnnf1octb  45195  nnfoctbdj  46461  fcoreslem4  47071  fcoresf1  47074  fargshiftfo  47447  fonex  48859