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

Theorem f1ofn 6036
Description: A one-to-one onto mapping is function on its domain. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1ofn (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)

Proof of Theorem f1ofn
StepHypRef Expression
1 f1of 6035 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
2 ffn 5944 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 5785  wf 5786  1-1-ontowf1o 5789
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 196  df-an 385  df-f 5794  df-f1 5795  df-f1o 5797
This theorem is referenced by:  f1ofun  6037  f1odm  6039  fveqf1o  6435  isomin  6465  isoini  6466  isofrlem  6468  isoselem  6469  weniso  6482  bren  7828  enfixsn  7932  phplem4  8005  php3  8009  domunfican  8096  fiint  8100  supisolem  8240  ordiso2  8281  unxpwdom2  8354  wemapwe  8455  infxpenlem  8697  ackbij2lem2  8923  ackbij2lem3  8924  fpwwe2lem9  9317  canthp1lem2  9332  hashfacen  13050  hashf1lem1  13051  fprodss  14466  phimullem  15271  unbenlem  15399  0ram  15511  symgfixelsi  17627  symgfixf1  17629  f1omvdmvd  17635  f1omvdcnv  17636  f1omvdconj  17638  f1otrspeq  17639  symggen  17662  psgnunilem1  17685  dprdf1o  18203  znleval  19670  znunithash  19680  mdetdiaglem  20171  basqtop  21272  tgqtop  21273  reghmph  21354  ordthmeolem  21362  qtophmeo  21378  imasf1oxmet  21938  imasf1omet  21939  imasf1obl  22051  imasf1oxms  22052  cnheiborlem  22509  ovolctb  23010  mbfimaopnlem  23173  logblog  24275  axcontlem5  25594  vdgr1d  26224  vdgr1b  26225  vdgr1a  26227  eupai  26288  eupatrl  26289  eupap1  26297  eupath2lem3  26300  vdegp1ai  26305  vdegp1bi  26306  nvinvfval  26673  adjbd1o  28122  isoun  28656  psgnfzto1stlem  28975  indf1ofs  29209  esumiun  29277  eulerpartgbij  29555  eulerpartlemgh  29561  ballotlemsima  29698  derangenlem  30201  subfacp1lem3  30212  subfacp1lem4  30213  subfacp1lem5  30214  fv1stcnv  30719  fv2ndcnv  30720  poimirlem1  32374  poimirlem2  32375  poimirlem3  32376  poimirlem4  32377  poimirlem6  32379  poimirlem7  32380  poimirlem8  32381  poimirlem9  32382  poimirlem13  32386  poimirlem14  32387  poimirlem15  32388  poimirlem16  32389  poimirlem17  32390  poimirlem19  32392  poimirlem20  32393  poimirlem23  32396  ltrnid  34233  ltrneq2  34246  cdleme51finvN  34656  diaintclN  35159  dibintclN  35268  mapdcl  35754  kelac1  36445  gicabl  36481  brco2f1o  37144  brco3f1o  37145  ntrclsfv1  37167  ntrneifv1  37191  clsneikex  37218  clsneinex  37219  neicvgmex  37229  neicvgel1  37231  stoweidlem27  38714
  Copyright terms: Public domain W3C validator