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

Theorem f1ofn 5473
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 5472 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
2 ffn 5389 . 2  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 15 1  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    Fn wfn 5250   -->wf 5251   -1-1-onto->wf1o 5254
This theorem is referenced by:  f1ofun  5474  f1odm  5476  fveqf1o  5806  isomin  5834  isoini  5835  isofrlem  5837  isoselem  5838  weniso  5852  bren  6871  phplem4  7043  php3  7047  domunfican  7129  fiint  7133  supisolem  7221  ordiso2  7230  unxpwdom2  7302  wemapwe  7400  infxpenlem  7641  ackbij2lem2  7866  ackbij2lem3  7867  fpwwe2lem9  8260  canthp1lem2  8275  hashfacen  11392  hashf1lem1  11393  phimullem  12847  unbenlem  12955  0ram  13067  dprdf1o  15267  znleval  16508  znunithash  16518  basqtop  17402  tgqtop  17403  reghmph  17484  ordthmeolem  17492  qtophmeo  17508  imasf1oxmet  17939  imasf1omet  17940  imasf1obl  18034  imasf1oxms  18035  cnheiborlem  18452  ovolctb  18849  mbfimaopnlem  19010  nvinvfval  21198  adjbd1o  22665  ballotlemsima  23074  isoun  23242  indf1ofs  23609  derangenlem  23702  subfacp1lem3  23713  subfacp1lem4  23714  subfacp1lem5  23715  eupai  23883  vdgr1d  23894  vdgr1b  23895  vdgr1a  23897  eupap1  23900  eupath2lem3  23903  vdegp1ai  23908  vdegp1bi  23909  axcontlem5  24596  cbicp  25166  caytr  25400  ltrinvlem  25406  kelac1  27161  enfixsn  27257  gicabl  27263  f1omvdmvd  27386  f1omvdcnv  27387  f1omvdconj  27389  f1otrspeq  27390  symggen  27411  psgnunilem1  27416  stoweidlem27  27776  ltrnid  30324  ltrneq2  30337  cdleme51finvN  30745  diaintclN  31248  dibintclN  31357  mapdcl  31843
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 177  df-an 360  df-f 5259  df-f1 5260  df-f1o 5262
  Copyright terms: Public domain W3C validator