Theorem fofn 6592

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

Syntax hints:   → wi 4   Fn wfn 6350  –onto→wfo 6353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952  df-f 6359  df-fo 6361

This theorem is referenced by:  fodmrnu  6598  foun  6633  fo00  6650  foelrni  6727  cbvfo  7045  foeqcnvco  7056  canth  7111  br1steqg  7711  br2ndeqg  7712  1stcof  7719  2ndcof  7720  df1st2  7793  df2nd2  7794  1stconst  7795  2ndconst  7796  fsplit  7812  fsplitOLD  7813  smoiso2  8006  fodomfi  8797  brwdom2  9037  fodomfi2  9486  fpwwe  10068  imasaddfnlem  16801  imasvscafn  16810  imasleval  16814  dmaf  17309  cdaf  17310  imasmnd2  17948  imasgrp2  18214  efgrelexlemb  18876  efgredeu  18878  imasring  19369  znf1o  20698  zzngim  20699  indlcim  20984  1stcfb  22053  upxp  22231  uptx  22233  cnmpt1st  22276  cnmpt2nd  22277  qtoptopon  22312  qtopcld  22321  qtopeu  22324  qtoprest  22325  imastopn  22328  qtophmeo  22425  elfm3  22558  uniiccdif  24179  dirith  26105  grporn  28298  0vfval  28383  foresf1o  30265  xppreima2  30395  1stpreimas  30441  1stpreima  30442  2ndpreima  30443  fsuppcurry1  30461  fsuppcurry2  30462  ffsrn  30465  gsummpt2d  30687  qusker  30918  imaslmod  30922  qtopt1  31099  qtophaus  31100  circcn  31102  cnre2csqima  31154  sigapildsys  31421  carsgclctunlem3  31578  nosupno  33203  nosupbday  33205  noetalem3  33219  bdayfn  33243  fnbigcup  33362  filnetlem4  33729  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  ssnnf1octb  41505  nnfoctbdj  42787  fargshiftfo  43651