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

Theorem f1of1 5632
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 5420 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
21simplbi 447 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 5410   -onto->wfo 5411   -1-1-onto->wf1o 5412
This theorem is referenced by:  f1of  5633  f1ocnvfvrneq  5978  isores3  6014  isoini2  6018  isosolem  6026  f1oiso  6030  weniso  6034  weisoeq  6035  f1opw2  6257  tposf12  6463  oacomf1olem  6766  enssdom  7091  domssex2  7226  mapen  7230  ssenen  7240  phplem4  7248  php3  7252  sucdom2  7262  ssfi  7288  f1finf1o  7294  domunfican  7338  fiint  7342  f1opwfi  7368  marypha1lem  7396  ordtypelem10  7452  oiexg  7460  unxpwdom2  7512  mapfien  7609  wemapwe  7610  isinffi  7835  infxpenlem  7851  fseqenlem1  7861  dfac12lem2  7980  dfac12r  7982  ackbij2  8079  cff1  8094  infpssrlem4  8142  fin4en1  8145  enfin2i  8157  fin23lem28  8176  isf32lem7  8195  isf34lem3  8211  enfin1ai  8220  canthnum  8480  canthwe  8482  canthp1lem2  8484  pwfseqlem4  8493  pwfseqlem5  8494  tskuni  8614  grothomex  8660  seqf1olem1  11317  hashfacen  11658  hashf1lem1  11659  fsumss  12474  ackbijnn  12562  bitsinv2  12910  bitsf1  12913  sadasslem  12937  sadeq  12939  phimullem  13123  eulerthlem2  13126  unbenlem  13231  f1ocpbllem  13704  f1ovscpbl  13706  xpsff1o2  13751  xpsmnd  14690  xpsgrp  14892  eqgen  14948  conjsubgen  14993  subggim  15008  gicsubgen  15020  odngen  15166  sylow1lem2  15188  sylow2blem1  15209  gsumzres  15472  gsumzcl  15473  gsumzf1o  15474  gsumzaddlem  15481  gsumconst  15487  gsumzmhm  15488  gsumzoppg  15494  dprdf1o  15545  coe1sfi  16565  coe1mul2lem2  16616  gsumfsum  16721  zntoslem  16792  znunithash  16800  iporthcom  16821  resthauslem  17381  sshauslem  17390  basqtop  17696  tgqtop  17697  hmeoopn  17751  hmeocld  17752  hmeontr  17754  hmeoimaf1o  17755  haushmphlem  17772  tsmsf1o  18127  imasdsf1olem  18356  imasf1oxmet  18358  imasf1oxms  18472  ovoliunlem1  19351  dyadmbl  19445  vitalilem3  19455  dvcnvlem  19813  dvne0f1  19849  dvcnvrelem2  19855  logf1o2  20494  dvlog  20495  wilthlem3  20806  usgraf1  21336  uslgra1  21345  usgra1  21346  usgraexmpl  21373  edgusgranbfin  21412  cusgraexilem2  21429  sizeusglecusglem1  21446  2trllemE  21506  constr1trl  21541  constr3trllem2  21591  eupatrl  21643  eupares  21650  eupath2lem3  21654  adjbd1o  23541  tpr2rico  24263  qqhre  24339  indf1ofs  24376  ballotlemscr  24729  ballotlemro  24733  ballotlemfrc  24737  ballotlemrinv0  24743  derangenlem  24810  subfacp1lem3  24821  subfacp1lem5  24823  erdsze2lem1  24842  cvmliftmolem1  24921  cvmlift2lem9a  24943  ghomf1olem  25058  fprodss  25227  axcontlem10  25816  mblfinlem  26143  metf1o  26351  ismtyima  26402  ismtyres  26407  rngoisocnv  26487  eldioph2lem2  26709  eldioph2  26710  pwfi2f1o  27128  gicabl  27131  lindfres  27161  islindf3  27164  lindsmm  27166  lmimlbs  27174  lbslcic  27179  f1omvdmvd  27254  f1omvdconj  27257  pmtrfconj  27275  usgra2adedgspthlem2  28044  laut11  30568  diaf1oN  31613  mapdcnvcl  32135  mapdcnvid2  32140
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 178  df-an 361  df-f1o 5420
  Copyright terms: Public domain W3C validator