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

Theorem fofn 6754
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 6752 . 2 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
21ffnd 6665 1 (𝐹:𝐴onto𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6487  ontowfo 6490
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3446  df-in 3916  df-ss 3926  df-f 6496  df-fo 6498
This theorem is referenced by:  fodmrnu  6760  foun  6798  fo00  6816  foelcdmi  6900  cbvfo  7230  foeqcnvco  7241  canth  7303  br1steqg  7934  br2ndeqg  7935  1stcof  7942  2ndcof  7943  df1st2  8019  df2nd2  8020  1stconst  8021  2ndconst  8022  fsplit  8038  smoiso2  8283  fodomfi  9203  brwdom2  9443  fodomfi2  9930  fpwwe  10516  imasaddfnlem  17345  imasvscafn  17354  imasleval  17358  dmaf  17870  cdaf  17871  imasmnd2  18528  imasgrp2  18796  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  29249  0vfval  29334  foresf1o  31216  2ndimaxp  31348  2ndresdju  31350  xppreima2  31352  1stpreimas  31402  1stpreima  31403  2ndpreima  31404  fsuppcurry1  31424  fsuppcurry2  31425  ffsrn  31428  gsummpt2d  31673  qusker  31922  imaslmod  31926  qtopt1  32177  qtophaus  32178  circcn  32180  cnre2csqima  32253  sigapildsys  32522  carsgclctunlem3  32681  fnbigcup  34372  filnetlem4  34739  ovoliunnfl  36006  voliunnfl  36008  volsupnfl  36009  ssnnf1octb  43140  nnfoctbdj  44419  fcoreslem4  45018  fcoresf1  45021  fargshiftfo  45352
  Copyright terms: Public domain W3C validator