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

Theorem f1ofn 6357
Description: A one-to-one onto mapping is function on its domain. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1ofn (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)

Proof of Theorem f1ofn
StepHypRef Expression
1 f1of 6356 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
21ffnd 6257 1 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6096  1-1-ontowf1o 6100
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 199  df-an 386  df-f 6105  df-f1 6106  df-f1o 6108
This theorem is referenced by:  f1ofun  6358  f1odm  6360  fveqf1o  6785  isomin  6815  isoini  6816  isofrlem  6818  isoselem  6819  weniso  6832  bren  8204  enfixsn  8311  phplem4  8384  php3  8388  domunfican  8475  fiint  8479  supisolem  8621  ordiso2  8662  unxpwdom2  8735  wemapwe  8844  djuun  9038  infxpenlem  9122  ackbij2lem2  9350  ackbij2lem3  9351  fpwwe2lem9  9748  canthp1lem2  9763  hashfacen  13487  hashf1lem1  13488  fprodss  15015  phimullem  15817  unbenlem  15945  0ram  16057  symgfixelsi  18167  symgfixf1  18169  f1omvdmvd  18175  f1omvdcnv  18176  f1omvdconj  18178  f1otrspeq  18179  symggen  18202  psgnunilem1  18225  dprdf1o  18747  znleval  20224  znunithash  20234  mdetdiaglem  20730  basqtop  21843  tgqtop  21844  reghmph  21925  ordthmeolem  21933  qtophmeo  21949  imasf1oxmet  22508  imasf1omet  22509  imasf1obl  22621  imasf1oxms  22622  cnheiborlem  23081  ovolctb  23598  mbfimaopnlem  23763  logblog  24874  axcontlem5  26205  nvinvfval  28020  adjbd1o  29469  isoun  29997  fsumiunle  30093  psgnfzto1stlem  30366  indf1ofs  30604  esumiun  30672  eulerpartgbij  30950  eulerpartlemgh  30956  ballotlemsima  31094  derangenlem  31670  subfacp1lem3  31681  subfacp1lem4  31682  subfacp1lem5  31683  fv1stcnv  32192  fv2ndcnv  32193  poimirlem1  33899  poimirlem2  33900  poimirlem3  33901  poimirlem4  33902  poimirlem6  33904  poimirlem7  33905  poimirlem8  33906  poimirlem9  33907  poimirlem13  33911  poimirlem14  33912  poimirlem15  33913  poimirlem16  33914  poimirlem17  33915  poimirlem19  33917  poimirlem20  33918  poimirlem23  33921  ltrnid  36156  ltrneq2  36169  cdleme51finvN  36577  diaintclN  37079  dibintclN  37188  mapdcl  37674  kelac1  38418  gicabl  38454  brco2f1o  39112  brco3f1o  39113  ntrclsfv1  39135  ntrneifv1  39159  clsneikex  39186  clsneinex  39187  neicvgmex  39197  neicvgel1  39199  stoweidlem27  40987  isomushgr  42496  isomuspgrlem1  42497  isomuspgrlem2b  42499  isomuspgrlem2d  42501  isomuspgr  42504  isomgrtrlem  42508
  Copyright terms: Public domain W3C validator