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

Theorem fofn 6753
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 6751 . 2 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
21ffnd 6664 1 (𝐹:𝐴onto𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6486  ontowfo 6489
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3445  df-in 3915  df-ss 3925  df-f 6495  df-fo 6497
This theorem is referenced by:  fodmrnu  6759  foun  6797  fo00  6815  foelcdmi  6899  cbvfo  7229  foeqcnvco  7240  canth  7302  br1steqg  7933  br2ndeqg  7934  1stcof  7941  2ndcof  7942  df1st2  8018  df2nd2  8019  1stconst  8020  2ndconst  8021  fsplit  8037  smoiso2  8282  fodomfi  9202  brwdom2  9442  fodomfi2  9929  fpwwe  10515  imasaddfnlem  17344  imasvscafn  17353  imasleval  17357  dmaf  17869  cdaf  17870  imasmnd2  18527  imasgrp2  18795  efgrelexlemb  19461  efgredeu  19463  imasring  19968  znf1o  20881  zzngim  20882  indlcim  21169  1stcfb  22718  upxp  22896  uptx  22898  cnmpt1st  22941  cnmpt2nd  22942  qtoptopon  22977  qtopcld  22986  qtopeu  22989  qtoprest  22990  imastopn  22993  qtophmeo  23090  elfm3  23223  uniiccdif  24864  dirith  26799  nosupno  26973  nosupbday  26975  noinfno  26988  noinfbday  26990  noetasuplem4  27006  noetainflem4  27010  bdayfn  27035  grporn  29261  0vfval  29346  foresf1o  31228  2ndimaxp  31360  2ndresdju  31362  xppreima2  31364  1stpreimas  31414  1stpreima  31415  2ndpreima  31416  fsuppcurry1  31436  fsuppcurry2  31437  ffsrn  31440  gsummpt2d  31685  qusker  31934  imaslmod  31938  qtopt1  32189  qtophaus  32190  circcn  32192  cnre2csqima  32265  sigapildsys  32534  carsgclctunlem3  32693  fnbigcup  34381  filnetlem4  34748  ovoliunnfl  36015  voliunnfl  36017  volsupnfl  36018  ssnnf1octb  43171  nnfoctbdj  44450  fcoreslem4  45049  fcoresf1  45052  fargshiftfo  45383
  Copyright terms: Public domain W3C validator