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

Theorem fofn 6084
 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 6082 . 2 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
21ffnd 6013 1 (𝐹:𝐴onto𝐵𝐹 Fn 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   Fn wfn 5852  –onto→wfo 5855 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3567  df-ss 3574  df-f 5861  df-fo 5863 This theorem is referenced by:  fodmrnu  6090  foun  6122  fo00  6139  foelrni  6211  cbvfo  6509  foeqcnvco  6520  canth  6573  1stcof  7156  2ndcof  7157  df1st2  7223  df2nd2  7224  1stconst  7225  2ndconst  7226  fsplit  7242  smoiso2  7426  fodomfi  8199  brwdom2  8438  fodomfi2  8843  fpwwe  9428  imasaddfnlem  16128  imasvscafn  16137  imasleval  16141  dmaf  16639  cdaf  16640  imasmnd2  17267  imasgrp2  17470  efgrelexlemb  18103  efgredeu  18105  imasring  18559  znf1o  19840  zzngim  19841  indlcim  20119  1stcfb  21188  upxp  21366  uptx  21368  cnmpt1st  21411  cnmpt2nd  21412  qtoptopon  21447  qtopcld  21456  qtopeu  21459  qtoprest  21460  imastopn  21463  qtophmeo  21560  elfm3  21694  uniiccdif  23286  dirith  25152  grporn  27263  0vfval  27349  foresf1o  29231  xppreima2  29333  1stpreimas  29367  1stpreima  29368  2ndpreima  29369  ffsrn  29388  gsummpt2d  29608  qtopt1  29726  qtophaus  29727  circcn  29729  cnre2csqima  29781  sigapildsys  30048  carsgclctunlem3  30205  br1steq  31427  br2ndeq  31428  fnbigcup  31703  filnetlem4  32071  ovoliunnfl  33122  voliunnfl  33124  volsupnfl  33125  ssnnf1octb  38891  nnfoctbdj  40010  fargshiftfo  40706
 Copyright terms: Public domain W3C validator