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

Theorem f1ofn 5738
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 5737 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
2 ffn 5652 . 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 5504   -->wf 5505   -1-1-onto->wf1o 5508
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 369  df-f 5513  df-f1 5514  df-f1o 5516
This theorem is referenced by:  f1ofun  5739  f1odm  5741  fveqf1o  6124  isomin  6152  isoini  6153  isofrlem  6155  isoselem  6156  weniso  6169  bren  7462  enfixsn  7563  phplem4  7636  php3  7640  domunfican  7726  fiint  7730  supisolem  7864  ordiso2  7873  unxpwdom2  7947  wemapwe  8070  wemapweOLD  8071  infxpenlem  8322  ackbij2lem2  8551  ackbij2lem3  8552  fpwwe2lem9  8945  canthp1lem2  8960  hashfacen  12426  hashf1lem1  12427  fprodss  13776  phimullem  14330  unbenlem  14447  0ram  14559  symgfixelsi  16596  symgfixf1  16598  f1omvdmvd  16604  f1omvdcnv  16605  f1omvdconj  16607  f1otrspeq  16608  symggen  16631  psgnunilem1  16654  dprdf1o  17211  znleval  18703  znunithash  18713  mdetdiaglem  19204  basqtop  20316  tgqtop  20317  reghmph  20398  ordthmeolem  20406  qtophmeo  20422  imasf1oxmet  20982  imasf1omet  20983  imasf1obl  21095  imasf1oxms  21096  cnheiborlem  21558  ovolctb  22005  mbfimaopnlem  22166  logblog  23269  axcontlem5  24413  vdgr1d  25045  vdgr1b  25046  vdgr1a  25048  eupai  25109  eupatrl  25110  eupap1  25118  eupath2lem3  25121  vdegp1ai  25126  vdegp1bi  25127  nvinvfval  25673  adjbd1o  27141  isoun  27697  indf1ofs  28205  esumiun  28273  eulerpartgbij  28530  eulerpartlemgh  28536  ballotlemsima  28673  derangenlem  28840  subfacp1lem3  28851  subfacp1lem4  28852  subfacp1lem5  28853  kelac1  31211  gicabl  31251  stoweidlem27  32010  usgra2adedglem1  32709  ltrnid  36307  ltrneq2  36320  cdleme51finvN  36730  diaintclN  37233  dibintclN  37342  mapdcl  37828
  Copyright terms: Public domain W3C validator