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

Theorem fofn 6155
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 6153 . 2 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
21ffnd 6084 1 (𝐹:𝐴onto𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 5921  ontowfo 5924
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621  df-f 5930  df-fo 5932
This theorem is referenced by:  fodmrnu  6161  foun  6193  fo00  6210  foelrni  6283  cbvfo  6584  foeqcnvco  6595  canth  6648  br1steqg  7232  br2ndeqg  7233  1stcof  7240  2ndcof  7241  df1st2  7308  df2nd2  7309  1stconst  7310  2ndconst  7311  fsplit  7327  smoiso2  7511  fodomfi  8280  brwdom2  8519  fodomfi2  8921  fpwwe  9506  imasaddfnlem  16235  imasvscafn  16244  imasleval  16248  dmaf  16746  cdaf  16747  imasmnd2  17374  imasgrp2  17577  efgrelexlemb  18209  efgredeu  18211  imasring  18665  znf1o  19948  zzngim  19949  indlcim  20227  1stcfb  21296  upxp  21474  uptx  21476  cnmpt1st  21519  cnmpt2nd  21520  qtoptopon  21555  qtopcld  21564  qtopeu  21567  qtoprest  21568  imastopn  21571  qtophmeo  21668  elfm3  21801  uniiccdif  23392  dirith  25263  grporn  27503  0vfval  27589  foresf1o  29469  xppreima2  29578  1stpreimas  29611  1stpreima  29612  2ndpreima  29613  ffsrn  29632  gsummpt2d  29909  qtopt1  30030  qtophaus  30031  circcn  30033  cnre2csqima  30085  sigapildsys  30353  carsgclctunlem3  30510  nosupno  31974  nosupbday  31976  noetalem3  31990  bdayfn  32014  fnbigcup  32133  filnetlem4  32501  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  ssnnf1octb  39696  nnfoctbdj  40991  fargshiftfo  41703
  Copyright terms: Public domain W3C validator