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

Theorem f1ofn 5663
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 5662 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
2 ffn 5580 . 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 5434   -->wf 5435   -1-1-onto->wf1o 5438
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 5443  df-f1 5444  df-f1o 5446
This theorem is referenced by:  f1ofun  5664  f1odm  5666  fveqf1o  6021  isomin  6049  isoini  6050  isofrlem  6052  isoselem  6053  weniso  6066  bren  7340  enfixsn  7441  phplem4  7514  php3  7518  domunfican  7605  fiint  7609  supisolem  7741  ordiso2  7750  unxpwdom2  7824  wemapwe  7949  wemapweOLD  7950  infxpenlem  8201  ackbij2lem2  8430  ackbij2lem3  8431  fpwwe2lem9  8826  canthp1lem2  8841  hashfacen  12228  hashf1lem1  12229  phimullem  13875  unbenlem  13990  0ram  14102  symgfixelsi  15961  symgfixf1  15964  f1omvdmvd  15970  f1omvdcnv  15971  f1omvdconj  15973  f1otrspeq  15974  symggen  15997  psgnunilem1  16020  psgnran  16042  dprdf1o  16551  znleval  18009  znunithash  18019  zrhcofipsgn  18045  mdet1  18430  basqtop  19306  tgqtop  19307  reghmph  19388  ordthmeolem  19396  qtophmeo  19412  imasf1oxmet  19972  imasf1omet  19973  imasf1obl  20085  imasf1oxms  20086  cnheiborlem  20548  ovolctb  20995  mbfimaopnlem  21155  axcontlem5  23236  vdgr1d  23595  vdgr1b  23596  vdgr1a  23598  eupai  23610  eupatrl  23611  eupap1  23619  eupath2lem3  23622  vdegp1ai  23627  vdegp1bi  23628  nvinvfval  24042  adjbd1o  25511  isoun  26019  indf1ofs  26504  eulerpartgbij  26777  eulerpartlemgh  26783  ballotlemsima  26920  derangenlem  27081  subfacp1lem3  27092  subfacp1lem4  27093  subfacp1lem5  27094  fprodss  27483  kelac1  29442  gicabl  29480  stoweidlem27  29848  usgra2adedglem1  30334  mdetdiaglem  30932  ltrnid  33875  ltrneq2  33888  cdleme51finvN  34296  diaintclN  34799  dibintclN  34908  mapdcl  35394
  Copyright terms: Public domain W3C validator