Theorem fofn 6796

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 6532  –onto→wfo 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916  df-f 6541  df-fo 6543

This theorem is used by:  fodmrnu  6802  foun  6841  fo00  6859  foelcdmi  6944  cbvfo  7295  foeqcnvco  7306  canth  7372  br1steqg  8021  br2ndeqg  8022  1stcof  8029  2ndcof  8030  df1st2  8107  df2nd2  8108  1stconst  8109  2ndconst  8110  fsplit  8126  smoiso2  8370  fodomfi  9297  brwdom2  9560  fodomfi2  10132  fpwwe  10724  imasaddfnlem  17693  imasvscafn  17702  imasleval  17706  dmaf  18217  cdaf  18218  imasmgm2  18856  imasmnd2  18961  imasgrp2  19258  efgrelexlemb  19957  efgredeu  19959  imasrng  20392  imasring  20553  znf1o  21850  zzngim  21851  indlcim  22139  1stcfb  23756  upxp  23935  uptx  23937  cnmpt1st  23980  cnmpt2nd  23981  qtoptopon  24016  qtopcld  24025  qtopeu  24028  qtoprest  24029  imastopn  24032  qtophmeo  24129  elfm3  24262  uniiccdif  25892  dirith  27849  nosupno  28053  nosupbday  28055  noinfno  28068  noinfbday  28070  noetasuplem4  28086  noetainflem4  28090  bdayfn  28127  grporn  31116  0vfval  31201  foresf1o  33093  2ndimaxp  33233  2ndresdju  33236  xppreima2  33238  1stpreimas  33292  1stpreima  33293  2ndpreima  33294  fsuppcurry1  33309  fsuppcurry2  33310  ffsrn  33313  gsummpt2d  33603  qusker  33903  imaslmod  33907  qtopt1  34460  qtophaus  34461  circcn  34463  cnre2csqima  34536  sigapildsys  34788  carsgclctunlem3  34945  rankfn  35725  onvfowev  35878  fnbigcup  36643  filnetlem4  37149  ovoliunnfl  38560  voliunnfl  38562  volsupnfl  38563  ssnnf1octb  46178  nnfoctbdj  47435  fcoreslem4  48105  fcoresf1  48108  fargshiftfo  48493  fonex  49946