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

Theorem f1ofn 5678
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 5677 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
2 ffn 5594 . 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 5452   -->wf 5453   -1-1-onto->wf1o 5456
This theorem is referenced by:  f1ofun  5679  f1odm  5681  fveqf1o  6032  isomin  6060  isoini  6061  isofrlem  6063  isoselem  6064  weniso  6078  bren  7120  phplem4  7292  php3  7296  domunfican  7382  fiint  7386  supisolem  7478  ordiso2  7487  unxpwdom2  7559  wemapwe  7657  infxpenlem  7900  ackbij2lem2  8125  ackbij2lem3  8126  fpwwe2lem9  8518  canthp1lem2  8533  hashfacen  11708  hashf1lem1  11709  phimullem  13173  unbenlem  13281  0ram  13393  dprdf1o  15595  znleval  16840  znunithash  16850  basqtop  17748  tgqtop  17749  reghmph  17830  ordthmeolem  17838  qtophmeo  17854  imasf1oxmet  18410  imasf1omet  18411  imasf1obl  18523  imasf1oxms  18524  cnheiborlem  18984  ovolctb  19391  mbfimaopnlem  19550  vdgr1d  21679  vdgr1b  21680  vdgr1a  21682  eupai  21694  eupatrl  21695  eupap1  21703  eupath2lem3  21706  vdegp1ai  21711  vdegp1bi  21712  nvinvfval  22126  adjbd1o  23593  isoun  24094  indf1ofs  24428  ballotlemsima  24778  derangenlem  24862  subfacp1lem3  24873  subfacp1lem4  24874  subfacp1lem5  24875  fprodss  25279  axcontlem5  25912  kelac1  27152  enfixsn  27248  gicabl  27254  f1omvdmvd  27377  f1omvdcnv  27378  f1omvdconj  27380  f1otrspeq  27381  symggen  27402  psgnunilem1  27407  stoweidlem27  27766  usgra2adedglem1  28356  ltrnid  31006  ltrneq2  31019  cdleme51finvN  31427  diaintclN  31930  dibintclN  32039  mapdcl  32525
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 179  df-an 362  df-f 5461  df-f1 5462  df-f1o 5464
  Copyright terms: Public domain W3C validator