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

Theorem f1ofn 5667
Description: A one-to-one onto mapping is function on its domain. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1ofn  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )

Proof of Theorem f1ofn
StepHypRef Expression
1 f1of 5666 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
2 ffn 5583 . 2  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 16 1  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    Fn wfn 5441   -->wf 5442   -1-1-onto->wf1o 5445
This theorem is referenced by:  f1ofun  5668  f1odm  5670  fveqf1o  6021  isomin  6049  isoini  6050  isofrlem  6052  isoselem  6053  weniso  6067  bren  7109  phplem4  7281  php3  7285  domunfican  7371  fiint  7375  supisolem  7467  ordiso2  7476  unxpwdom2  7548  wemapwe  7646  infxpenlem  7887  ackbij2lem2  8112  ackbij2lem3  8113  fpwwe2lem9  8505  canthp1lem2  8520  hashfacen  11695  hashf1lem1  11696  phimullem  13160  unbenlem  13268  0ram  13380  dprdf1o  15582  znleval  16827  znunithash  16837  basqtop  17735  tgqtop  17736  reghmph  17817  ordthmeolem  17825  qtophmeo  17841  imasf1oxmet  18397  imasf1omet  18398  imasf1obl  18510  imasf1oxms  18511  cnheiborlem  18971  ovolctb  19378  mbfimaopnlem  19539  vdgr1d  21666  vdgr1b  21667  vdgr1a  21669  eupai  21681  eupatrl  21682  eupap1  21690  eupath2lem3  21693  vdegp1ai  21698  vdegp1bi  21699  nvinvfval  22113  adjbd1o  23580  isoun  24081  indf1ofs  24415  ballotlemsima  24765  derangenlem  24849  subfacp1lem3  24860  subfacp1lem4  24861  subfacp1lem5  24862  fprodss  25266  axcontlem5  25899  kelac1  27129  enfixsn  27225  gicabl  27231  f1omvdmvd  27354  f1omvdcnv  27355  f1omvdconj  27357  f1otrspeq  27358  symggen  27379  psgnunilem1  27384  stoweidlem27  27743  usgra2adedglem1  28271  ltrnid  30869  ltrneq2  30882  cdleme51finvN  31290  diaintclN  31793  dibintclN  31902  mapdcl  32388
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-f 5450  df-f1 5451  df-f1o 5453
  Copyright terms: Public domain W3C validator