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

Theorem f1ofn 5817
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 5816 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
2 ffn 5731 . 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 5583   -->wf 5584   -1-1-onto->wf1o 5587
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 5592  df-f1 5593  df-f1o 5595
This theorem is referenced by:  f1ofun  5818  f1odm  5820  fveqf1o  6194  isomin  6222  isoini  6223  isofrlem  6225  isoselem  6226  weniso  6239  bren  7526  enfixsn  7627  phplem4  7700  php3  7704  domunfican  7794  fiint  7798  supisolem  7932  ordiso2  7941  unxpwdom2  8015  wemapwe  8140  wemapweOLD  8141  infxpenlem  8392  ackbij2lem2  8621  ackbij2lem3  8622  fpwwe2lem9  9017  canthp1lem2  9032  hashfacen  12470  hashf1lem1  12471  phimullem  14171  unbenlem  14288  0ram  14400  symgfixelsi  16274  symgfixf1  16277  f1omvdmvd  16283  f1omvdcnv  16284  f1omvdconj  16286  f1otrspeq  16287  symggen  16310  psgnunilem1  16333  psgnran  16355  dprdf1o  16893  znleval  18400  znunithash  18410  zrhcofipsgn  18436  mdetdiaglem  18907  basqtop  20039  tgqtop  20040  reghmph  20121  ordthmeolem  20129  qtophmeo  20145  imasf1oxmet  20705  imasf1omet  20706  imasf1obl  20818  imasf1oxms  20819  cnheiborlem  21281  ovolctb  21728  mbfimaopnlem  21889  axcontlem5  24044  vdgr1d  24676  vdgr1b  24677  vdgr1a  24679  eupai  24740  eupatrl  24741  eupap1  24749  eupath2lem3  24752  vdegp1ai  24757  vdegp1bi  24758  nvinvfval  25308  adjbd1o  26777  isoun  27289  indf1ofs  27790  eulerpartgbij  28062  eulerpartlemgh  28068  ballotlemsima  28205  derangenlem  28366  subfacp1lem3  28377  subfacp1lem4  28378  subfacp1lem5  28379  fprodss  28933  kelac1  30840  gicabl  30878  stoweidlem27  31554  usgra2adedglem1  32050  ltrnid  35148  ltrneq2  35161  cdleme51finvN  35569  diaintclN  36072  dibintclN  36181  mapdcl  36667
  Copyright terms: Public domain W3C validator