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

Theorem f1ofn 5803
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 5802 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
2 ffn 5717 . 2  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 16 1  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    Fn wfn 5569   -->wf 5570   -1-1-onto->wf1o 5573
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 185  df-an 371  df-f 5578  df-f1 5579  df-f1o 5581
This theorem is referenced by:  f1ofun  5804  f1odm  5806  fveqf1o  6186  isomin  6214  isoini  6215  isofrlem  6217  isoselem  6218  weniso  6231  bren  7523  enfixsn  7624  phplem4  7697  php3  7701  domunfican  7791  fiint  7795  supisolem  7929  ordiso2  7938  unxpwdom2  8012  wemapwe  8137  wemapweOLD  8138  infxpenlem  8389  ackbij2lem2  8618  ackbij2lem3  8619  fpwwe2lem9  9014  canthp1lem2  9029  hashfacen  12477  hashf1lem1  12478  phimullem  14181  unbenlem  14298  0ram  14410  symgfixelsi  16329  symgfixf1  16331  f1omvdmvd  16337  f1omvdcnv  16338  f1omvdconj  16340  f1otrspeq  16341  symggen  16364  psgnunilem1  16387  dprdf1o  16947  znleval  18460  znunithash  18470  mdetdiaglem  18967  basqtop  20078  tgqtop  20079  reghmph  20160  ordthmeolem  20168  qtophmeo  20184  imasf1oxmet  20744  imasf1omet  20745  imasf1obl  20857  imasf1oxms  20858  cnheiborlem  21320  ovolctb  21767  mbfimaopnlem  21928  axcontlem5  24136  vdgr1d  24768  vdgr1b  24769  vdgr1a  24771  eupai  24832  eupatrl  24833  eupap1  24841  eupath2lem3  24844  vdegp1ai  24849  vdegp1bi  24850  nvinvfval  25400  adjbd1o  26869  isoun  27385  indf1ofs  27905  eulerpartgbij  28177  eulerpartlemgh  28183  ballotlemsima  28320  derangenlem  28481  subfacp1lem3  28492  subfacp1lem4  28493  subfacp1lem5  28494  fprodss  29048  kelac1  30977  gicabl  31015  stoweidlem27  31694  usgra2adedglem1  32190  ltrnid  35561  ltrneq2  35574  cdleme51finvN  35984  diaintclN  36487  dibintclN  36596  mapdcl  37082
  Copyright terms: Public domain W3C validator