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

Theorem f1ofn 5489
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 5488 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
2 ffn 5405 . 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 5266   -->wf 5267   -1-1-onto->wf1o 5270
This theorem is referenced by:  f1ofun  5490  f1odm  5492  fveqf1o  5822  isomin  5850  isoini  5851  isofrlem  5853  isoselem  5854  weniso  5868  bren  6887  phplem4  7059  php3  7063  domunfican  7145  fiint  7149  supisolem  7237  ordiso2  7246  unxpwdom2  7318  wemapwe  7416  infxpenlem  7657  ackbij2lem2  7882  ackbij2lem3  7883  fpwwe2lem9  8276  canthp1lem2  8291  hashfacen  11408  hashf1lem1  11409  phimullem  12863  unbenlem  12971  0ram  13083  dprdf1o  15283  znleval  16524  znunithash  16534  basqtop  17418  tgqtop  17419  reghmph  17500  ordthmeolem  17508  qtophmeo  17524  imasf1oxmet  17955  imasf1omet  17956  imasf1obl  18050  imasf1oxms  18051  cnheiborlem  18468  ovolctb  18865  mbfimaopnlem  19026  nvinvfval  21214  adjbd1o  22681  ballotlemsima  23090  isoun  23257  indf1ofs  23624  derangenlem  23717  subfacp1lem3  23728  subfacp1lem4  23729  subfacp1lem5  23730  eupai  23898  vdgr1d  23909  vdgr1b  23910  vdgr1a  23912  eupap1  23915  eupath2lem3  23918  vdegp1ai  23923  vdegp1bi  23924  axcontlem5  24668  cbicp  25269  caytr  25503  ltrinvlem  25509  kelac1  27264  enfixsn  27360  gicabl  27366  f1omvdmvd  27489  f1omvdcnv  27490  f1omvdconj  27492  f1otrspeq  27493  symggen  27514  psgnunilem1  27519  stoweidlem27  27879  eupatrl  28385  ltrnid  30946  ltrneq2  30959  cdleme51finvN  31367  diaintclN  31870  dibintclN  31979  mapdcl  32465
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 5275  df-f1 5276  df-f1o 5278
  Copyright terms: Public domain W3C validator