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

Theorem f1ofn 5635
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 5634 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
2 ffn 5552 . 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 5406   -->wf 5407   -1-1-onto->wf1o 5410
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 5415  df-f1 5416  df-f1o 5418
This theorem is referenced by:  f1ofun  5636  f1odm  5638  fveqf1o  5993  isomin  6021  isoini  6022  isofrlem  6024  isoselem  6025  weniso  6038  bren  7311  enfixsn  7412  phplem4  7485  php3  7489  domunfican  7576  fiint  7580  supisolem  7712  ordiso2  7721  unxpwdom2  7795  wemapwe  7920  wemapweOLD  7921  infxpenlem  8172  ackbij2lem2  8401  ackbij2lem3  8402  fpwwe2lem9  8797  canthp1lem2  8812  hashfacen  12199  hashf1lem1  12200  phimullem  13846  unbenlem  13961  0ram  14073  symgfixelsi  15929  symgfixf1  15932  f1omvdmvd  15938  f1omvdcnv  15939  f1omvdconj  15941  f1otrspeq  15942  symggen  15965  psgnunilem1  15988  psgnran  16010  dprdf1o  16515  znleval  17956  znunithash  17966  zrhcofipsgn  17992  mdet1  18377  basqtop  19253  tgqtop  19254  reghmph  19335  ordthmeolem  19343  qtophmeo  19359  imasf1oxmet  19919  imasf1omet  19920  imasf1obl  20032  imasf1oxms  20033  cnheiborlem  20495  ovolctb  20942  mbfimaopnlem  21102  axcontlem5  23159  vdgr1d  23518  vdgr1b  23519  vdgr1a  23521  eupai  23533  eupatrl  23534  eupap1  23542  eupath2lem3  23545  vdegp1ai  23550  vdegp1bi  23551  nvinvfval  23965  adjbd1o  25434  isoun  25942  indf1ofs  26430  eulerpartgbij  26703  eulerpartlemgh  26709  ballotlemsima  26846  derangenlem  27007  subfacp1lem3  27018  subfacp1lem4  27019  subfacp1lem5  27020  fprodss  27408  kelac1  29359  gicabl  29397  stoweidlem27  29765  usgra2adedglem1  30251  mdetdiaglem  30794  ltrnid  33530  ltrneq2  33543  cdleme51finvN  33951  diaintclN  34454  dibintclN  34563  mapdcl  35049
  Copyright terms: Public domain W3C validator