Theorem fofn 6799

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 6534  –onto→wfo 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896  df-f 6543  df-fo 6545

This theorem is used by:  fodmrnu  6805  foun  6844  fo00  6862  foelcdmi  6947  cbvfo  7298  foeqcnvco  7309  canth  7375  br1steqg  8024  br2ndeqg  8025  1stcof  8032  2ndcof  8033  df1st2  8112  df2nd2  8113  1stconst  8114  2ndconst  8115  fsplit  8131  smoiso2  8381  fodomfi  9308  brwdom2  9571  fodomfi2  10143  fpwwe  10735  imasaddfnlem  17706  imasvscafn  17715  imasleval  17719  dmaf  18230  cdaf  18231  imasmgm2  18869  imasmnd2  18974  imasgrp2  19271  efgrelexlemb  19970  efgredeu  19972  imasrng  20405  imasring  20566  znf1o  21863  zzngim  21864  indlcim  22152  1stcfb  23769  upxp  23948  uptx  23950  cnmpt1st  23993  cnmpt2nd  23994  qtoptopon  24029  qtopcld  24038  qtopeu  24041  qtoprest  24042  imastopn  24045  qtophmeo  24142  elfm3  24275  uniiccdif  25905  dirith  27862  nosupno  28066  nosupbday  28068  noinfno  28081  noinfbday  28083  noetasuplem4  28099  noetainflem4  28103  bdayfn  28140  grporn  31129  0vfval  31214  foresf1o  33148  2ndimaxp  33288  2ndresdju  33291  xppreima2  33293  1stpreimas  33347  1stpreima  33348  2ndpreima  33349  fsuppcurry1  33363  fsuppcurry2  33364  ffsrn  33367  gsummpt2d  33657  qusker  33957  imaslmod  33961  qtopt1  34514  qtophaus  34515  circcn  34517  cnre2csqima  34590  sigapildsys  34842  carsgclctunlem3  34999  rankfn  35789  onvfowev  35970  fnbigcup  36756  filnetlem4  37262  ovoliunnfl  38674  voliunnfl  38676  volsupnfl  38677  ssnnf1octb  46303  nnfoctbdj  47560  fcoreslem4  48230  fcoresf1  48233  fargshiftfo  48618  fonex  50072