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

Theorem f1of1 5471
Description: A one-to-one onto mapping is a one-to-one mapping. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1of1  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )

Proof of Theorem f1of1
StepHypRef Expression
1 df-f1o 5262 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
21simplbi 446 1  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   -1-1->wf1 5252   -onto->wfo 5253   -1-1-onto->wf1o 5254
This theorem is referenced by:  f1of  5472  isores3  5832  isoini2  5836  isosolem  5844  f1oiso  5848  weniso  5852  weisoeq  5853  f1opw2  6071  tposf12  6259  oacomf1olem  6562  enssdom  6886  domssex2  7021  mapen  7025  ssenen  7035  phplem4  7043  php3  7047  sucdom2  7057  ssfi  7083  f1finf1o  7086  domunfican  7129  fiint  7133  f1opwfi  7159  marypha1lem  7186  ordtypelem10  7242  oiexg  7250  unxpwdom2  7302  mapfien  7399  wemapwe  7400  isinffi  7625  infxpenlem  7641  fseqenlem1  7651  dfac12lem2  7770  dfac12r  7772  ackbij2  7869  cff1  7884  infpssrlem4  7932  fin4en1  7935  enfin2i  7947  fin23lem28  7966  isf32lem7  7985  isf34lem3  8001  enfin1ai  8010  canthnum  8271  canthwe  8273  canthp1lem2  8275  pwfseqlem4  8284  pwfseqlem5  8285  tskuni  8405  grothomex  8451  seqf1olem1  11085  hashfacen  11392  hashf1lem1  11393  fsumss  12198  ackbijnn  12286  bitsinv2  12634  bitsf1  12637  sadasslem  12661  sadeq  12663  phimullem  12847  eulerthlem2  12850  unbenlem  12955  f1ocpbllem  13426  f1ovscpbl  13428  xpsff1o2  13473  xpsmnd  14412  xpsgrp  14614  eqgen  14670  conjsubgen  14715  subggim  14730  gicsubgen  14742  odngen  14888  sylow1lem2  14910  sylow2blem1  14931  gsumzres  15194  gsumzcl  15195  gsumzf1o  15196  gsumzaddlem  15203  gsumconst  15209  gsumzmhm  15210  gsumzoppg  15216  dprdf1o  15267  coe1sfi  16293  coe1mul2lem2  16345  gsumfsum  16439  zntoslem  16510  znunithash  16518  iporthcom  16539  resthauslem  17091  sshauslem  17100  basqtop  17402  tgqtop  17403  hmeoopn  17457  hmeocld  17458  hmeontr  17460  hmeoimaf1o  17461  haushmphlem  17478  tsmsf1o  17827  imasdsf1olem  17937  imasf1oxmet  17939  imasf1oxms  18035  ovoliunlem1  18861  dyadmbl  18955  vitalilem3  18965  dvcnvlem  19323  dvne0f1  19359  dvcnvrelem2  19365  logf1o2  19997  dvlog  19998  wilthlem3  20308  adjbd1o  22665  ballotlemscr  23077  ballotlemro  23081  ballotlemfrc  23085  ballotlemrinv0  23091  tpr2rico  23296  indf1ofs  23609  derangenlem  23702  subfacp1lem3  23713  subfacp1lem5  23715  erdsze2lem1  23734  cvmliftmolem1  23812  cvmlift2lem9a  23834  eupares  23899  eupath2lem3  23903  ghomf1olem  24001  axcontlem10  24601  f2imacnv  25052  grpodlcan  25376  grpodivzer  25377  metf1o  26469  ismtyima  26527  ismtyres  26532  rngoisocnv  26612  eldioph2lem2  26840  eldioph2  26841  pwfi2f1o  27260  gicabl  27263  lindfres  27293  islindf3  27296  lindsmm  27298  lmimlbs  27306  lbslcic  27311  f1omvdmvd  27386  f1omvdconj  27389  pmtrfconj  27407  uslgra1  28118  usgra1  28119  usgraexmpl  28133  laut11  30275  diaf1oN  31320  mapdcnvcl  31842  mapdcnvid2  31847
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-f1o 5262
  Copyright terms: Public domain W3C validator