MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fofn Structured version   Visualization version   GIF version

Theorem fofn 6302
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
StepHypRef Expression
1 fof 6300 . 2 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
21ffnd 6226 1 (𝐹:𝐴onto𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6065  ontowfo 6068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-in 3741  df-ss 3748  df-f 6074  df-fo 6076
This theorem is referenced by:  fodmrnu  6308  foun  6340  fo00  6357  foelrni  6435  cbvfo  6738  foeqcnvco  6749  canth  6802  br1steqg  7390  br2ndeqg  7391  1stcof  7398  2ndcof  7399  df1st2  7467  df2nd2  7468  1stconst  7469  2ndconst  7470  fsplit  7486  smoiso2  7672  fodomfi  8448  brwdom2  8687  fodomfi2  9136  fpwwe  9723  imasaddfnlem  16457  imasvscafn  16466  imasleval  16470  dmaf  16967  cdaf  16968  imasmnd2  17596  imasgrp2  17800  efgrelexlemb  18432  efgredeu  18434  imasring  18889  znf1o  20175  zzngim  20176  indlcim  20458  1stcfb  21531  upxp  21709  uptx  21711  cnmpt1st  21754  cnmpt2nd  21755  qtoptopon  21790  qtopcld  21799  qtopeu  21802  qtoprest  21803  imastopn  21806  qtophmeo  21903  elfm3  22036  uniiccdif  23639  dirith  25512  grporn  27835  0vfval  27920  foresf1o  29795  xppreima2  29903  1stpreimas  29935  1stpreima  29936  2ndpreima  29937  ffsrn  29956  gsummpt2d  30231  qtopt1  30352  qtophaus  30353  circcn  30355  cnre2csqima  30407  sigapildsys  30675  carsgclctunlem3  30832  nosupno  32296  nosupbday  32298  noetalem3  32312  bdayfn  32336  fnbigcup  32455  filnetlem4  32822  ovoliunnfl  33878  voliunnfl  33880  volsupnfl  33881  ssnnf1octb  40032  nnfoctbdj  41313  fargshiftfo  42115
  Copyright terms: Public domain W3C validator