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

Theorem f1ofn 5820
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 5819 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
2 ffn 5733 . 2  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 17 1  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    Fn wfn 5580   -->wf 5581   -1-1-onto->wf1o 5584
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 189  df-an 373  df-f 5589  df-f1 5590  df-f1o 5592
This theorem is referenced by:  f1ofun  5821  f1odm  5823  fveqf1o  6205  isomin  6233  isoini  6234  isofrlem  6236  isoselem  6237  weniso  6250  bren  7583  enfixsn  7686  phplem4  7759  php3  7763  domunfican  7849  fiint  7853  supisolem  7994  ordiso2  8035  unxpwdom2  8108  wemapwe  8207  infxpenlem  8449  ackbij2lem2  8675  ackbij2lem3  8676  fpwwe2lem9  9068  canthp1lem2  9083  hashfacen  12624  hashf1lem1  12625  fprodss  14014  phimullem  14739  unbenlem  14864  0ram  14990  symgfixelsi  17088  symgfixf1  17090  f1omvdmvd  17096  f1omvdcnv  17097  f1omvdconj  17099  f1otrspeq  17100  symggen  17123  psgnunilem1  17146  dprdf1o  17677  znleval  19137  znunithash  19147  mdetdiaglem  19635  basqtop  20738  tgqtop  20739  reghmph  20820  ordthmeolem  20828  qtophmeo  20844  imasf1oxmet  21402  imasf1omet  21403  imasf1obl  21515  imasf1oxms  21516  cnheiborlem  21994  ovolctb  22455  mbfimaopnlem  22623  logblog  23741  axcontlem5  25010  vdgr1d  25643  vdgr1b  25644  vdgr1a  25646  eupai  25707  eupatrl  25708  eupap1  25716  eupath2lem3  25719  vdegp1ai  25724  vdegp1bi  25725  nvinvfval  26273  adjbd1o  27750  isoun  28294  psgnfzto1stlem  28625  indf1ofs  28859  esumiun  28927  eulerpartgbij  29217  eulerpartlemgh  29223  ballotlemsima  29360  ballotlemsimaOLD  29398  derangenlem  29906  subfacp1lem3  29917  subfacp1lem4  29918  subfacp1lem5  29919  fv1stcnv  30434  fv2ndcnv  30435  poimirlem1  31953  poimirlem2  31954  poimirlem3  31955  poimirlem4  31956  poimirlem6  31958  poimirlem7  31959  poimirlem8  31960  poimirlem9  31961  poimirlem13  31965  poimirlem14  31966  poimirlem15  31967  poimirlem16  31968  poimirlem17  31969  poimirlem19  31971  poimirlem20  31972  poimirlem23  31975  ltrnid  33712  ltrneq2  33725  cdleme51finvN  34135  diaintclN  34638  dibintclN  34747  mapdcl  35233  kelac1  35933  gicabl  35969  stoweidlem27  37897  usgra2adedglem1  39774
  Copyright terms: Public domain W3C validator