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

Theorem f1ofn 6610
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 6609 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
21ffnd 6509 1 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6344  1-1-ontowf1o 6348
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 208  df-an 397  df-f 6353  df-f1 6354  df-f1o 6356
This theorem is referenced by:  f1ofun  6611  f1odm  6613  fveqf1o  7049  isomin  7079  isoini  7080  isofrlem  7082  isoselem  7083  weniso  7096  bren  8507  enfixsn  8615  phplem4  8688  php3  8692  domunfican  8780  fiint  8784  supisolem  8926  ordiso2  8968  unxpwdom2  9041  wemapwe  9149  djuun  9344  infxpenlem  9428  ackbij2lem2  9651  ackbij2lem3  9652  fpwwe2lem9  10049  canthp1lem2  10064  hashfacen  13802  hashf1lem1  13803  fprodss  15292  phimullem  16106  unbenlem  16234  0ram  16346  symgfixelsi  18494  symgfixf1  18496  f1omvdmvd  18502  f1omvdcnv  18503  f1omvdconj  18505  f1otrspeq  18506  symggen  18529  psgnunilem1  18552  dprdf1o  19085  znleval  20631  znunithash  20641  mdetdiaglem  21137  basqtop  22249  tgqtop  22250  reghmph  22331  ordthmeolem  22339  qtophmeo  22355  imasf1oxmet  22914  imasf1omet  22915  imasf1obl  23027  imasf1oxms  23028  cnheiborlem  23487  ovolctb  24020  mbfimaopnlem  24185  logblog  25297  axcontlem5  26682  nvinvfval  28345  adjbd1o  29790  isoun  30364  fsumiunle  30473  symgcom  30655  pmtrcnel  30661  psgnfzto1stlem  30670  tocycfvres1  30680  tocycfvres2  30681  cycpmfvlem  30682  cycpmfv3  30685  cycpmconjvlem  30711  cycpmrn  30713  cycpmconjslem2  30725  indf1ofs  31185  esumiun  31253  eulerpartgbij  31530  eulerpartlemgh  31536  ballotlemsima  31673  derangenlem  32316  subfacp1lem3  32327  subfacp1lem4  32328  subfacp1lem5  32329  fv1stcnv  32918  fv2ndcnv  32919  poimirlem1  34775  poimirlem2  34776  poimirlem3  34777  poimirlem4  34778  poimirlem6  34780  poimirlem7  34781  poimirlem8  34782  poimirlem9  34783  poimirlem13  34787  poimirlem14  34788  poimirlem15  34789  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem23  34797  ltrnid  37153  ltrneq2  37166  cdleme51finvN  37574  diaintclN  38076  dibintclN  38185  mapdcl  38671  kelac1  39543  gicabl  39579  brco2f1o  40262  brco3f1o  40263  ntrclsfv1  40285  ntrneifv1  40309  clsneikex  40336  clsneinex  40337  neicvgmex  40347  neicvgel1  40349  stoweidlem27  42193  isomushgr  43838  isomuspgrlem1  43839  isomuspgrlem2b  43841  isomuspgrlem2d  43843  isomuspgr  43846  isomgrtrlem  43850
  Copyright terms: Public domain W3C validator