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

Theorem f1ofn 6615
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 6614 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
21ffnd 6514 1 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6349  1-1-ontowf1o 6353
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 6358  df-f1 6359  df-f1o 6361
This theorem is referenced by:  f1ofun  6616  f1odm  6618  fveqf1o  7054  isomin  7084  isoini  7085  isofrlem  7087  isoselem  7088  weniso  7101  bren  8512  enfixsn  8620  phplem4  8693  php3  8697  domunfican  8785  fiint  8789  supisolem  8931  ordiso2  8973  unxpwdom2  9046  wemapwe  9154  djuun  9349  infxpenlem  9433  ackbij2lem2  9656  ackbij2lem3  9657  fpwwe2lem9  10054  canthp1lem2  10069  hashfacen  13807  hashf1lem1  13808  fprodss  15297  phimullem  16111  unbenlem  16239  0ram  16351  symgfixelsi  18499  symgfixf1  18501  f1omvdmvd  18507  f1omvdcnv  18508  f1omvdconj  18510  f1otrspeq  18511  symggen  18534  psgnunilem1  18557  dprdf1o  19090  znleval  20636  znunithash  20646  mdetdiaglem  21142  basqtop  22254  tgqtop  22255  reghmph  22336  ordthmeolem  22344  qtophmeo  22360  imasf1oxmet  22919  imasf1omet  22920  imasf1obl  23032  imasf1oxms  23033  cnheiborlem  23492  ovolctb  24025  mbfimaopnlem  24190  logblog  25302  axcontlem5  26687  nvinvfval  28350  adjbd1o  29795  isoun  30369  fsumiunle  30478  symgcom  30660  pmtrcnel  30666  psgnfzto1stlem  30675  tocycfvres1  30685  tocycfvres2  30686  cycpmfvlem  30687  cycpmfv3  30690  cycpmconjvlem  30716  cycpmrn  30718  cycpmconjslem2  30730  indf1ofs  31190  esumiun  31258  eulerpartgbij  31535  eulerpartlemgh  31541  ballotlemsima  31678  derangenlem  32321  subfacp1lem3  32332  subfacp1lem4  32333  subfacp1lem5  32334  fv1stcnv  32923  fv2ndcnv  32924  poimirlem1  34779  poimirlem2  34780  poimirlem3  34781  poimirlem4  34782  poimirlem6  34784  poimirlem7  34785  poimirlem8  34786  poimirlem9  34787  poimirlem13  34791  poimirlem14  34792  poimirlem15  34793  poimirlem16  34794  poimirlem17  34795  poimirlem19  34797  poimirlem20  34798  poimirlem23  34801  ltrnid  37157  ltrneq2  37170  cdleme51finvN  37578  diaintclN  38080  dibintclN  38189  mapdcl  38675  kelac1  39547  gicabl  39583  brco2f1o  40266  brco3f1o  40267  ntrclsfv1  40289  ntrneifv1  40313  clsneikex  40340  clsneinex  40341  neicvgmex  40351  neicvgel1  40353  stoweidlem27  42197  isomushgr  43842  isomuspgrlem1  43843  isomuspgrlem2b  43845  isomuspgrlem2d  43847  isomuspgr  43850  isomgrtrlem  43854
  Copyright terms: Public domain W3C validator