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

Theorem f1of1 5830
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 5608 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
21simplbi 461 1  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   -1-1->wf1 5598   -onto->wfo 5599   -1-1-onto->wf1o 5600
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 188  df-an 372  df-f1o 5608
This theorem is referenced by:  f1of  5831  f1oresrab  6070  f1prex  6197  f1ocnvfvrneq  6199  isores3  6241  isoini2  6245  isosolem  6253  f1oiso  6257  weniso  6260  weisoeq  6261  f1opw2  6536  f1ovv  6778  tposf12  7009  oacomf1olem  7276  enssdom  7604  domssex2  7741  mapen  7745  ssenen  7755  phplem4  7763  php3  7767  sucdom2  7777  ssfi  7801  f1finf1o  7807  domunfican  7853  fiint  7857  f1opwfi  7887  mapfienlem1  7927  mapfienlem2  7928  mapfien  7930  marypha1lem  7956  ordtypelem10  8051  oiexg  8059  unxpwdom2  8112  wemapwe  8210  isinffi  8434  infxpenlem  8452  fseqenlem1  8462  dfac12lem2  8581  dfac12r  8583  ackbij2  8680  cff1  8695  infpssrlem4  8743  fin4en1  8746  enfin2i  8758  fin23lem28  8777  isf32lem7  8796  isf34lem3  8812  enfin1ai  8821  canthnum  9081  canthwe  9083  canthp1lem2  9085  pwfseqlem4  9094  pwfseqlem5  9095  tskuni  9215  grothomex  9261  negfi  10561  seqf1olem1  12258  hashfacen  12621  hashf1lem1  12622  fsumss  13790  ackbijnn  13885  fprodss  14001  bitsinv2  14416  bitsf1  14419  sadasslem  14443  sadeq  14445  phimullem  14726  eulerthlem2  14729  unbenlem  14851  f1ocpbllem  15429  f1ovscpbl  15431  xpsff1o2  15476  xpsmnd  16575  xpsgrp  16804  eqgen  16869  conjsubgen  16914  subggim  16929  gicsubgen  16941  symgfvne  17028  symgextf1  17061  symgfixelsi  17075  f1omvdmvd  17083  f1omvdconj  17086  pmtrfconj  17106  odngen  17225  sylow1lem2  17250  sylow2blem1  17271  gsumzres  17542  gsumzcl2  17543  gsumzf1o  17545  gsumzaddlem  17553  gsumconst  17566  gsumzmhm  17569  gsumzoppg  17576  dprdf1o  17664  rim0to0  17969  coe1sfi  18805  coe1mul2lem2  18860  gsumfsum  19033  zntoslem  19125  znunithash  19133  iporthcom  19200  lindfres  19379  islindf3  19382  lindsmm  19384  lmimlbs  19392  lbslcic  19397  resthauslem  20377  sshauslem  20386  basqtop  20724  tgqtop  20725  hmeoopn  20779  hmeocld  20780  hmeontr  20782  hmeoimaf1o  20783  haushmphlem  20800  tsmsf1o  21157  imasdsf1olem  21386  imasf1oxmet  21388  imasf1oxms  21502  ovoliunlem1  22453  dyadmbl  22556  vitalilem3  22566  dvcnvlem  22926  dvne0f1  22962  dvcnvrelem2  22968  logf1o2  23593  dvlog  23594  wilthlem3  23993  istrkg2ld  24506  f1otrg  24899  axcontlem10  25001  usgraf1  25085  uslgra1  25097  usgra1  25098  usgraexmplef  25126  edgusgranbfin  25176  cusgraexilem2  25193  sizeusglecusglem1  25210  2trllemE  25281  constr1trl  25316  usgra2adedgspthlem2  25338  constr3trllem2  25377  eupatrl  25694  eupares  25701  eupath2lem3  25705  adjbd1o  27736  padct  28313  madjusmdetlem4  28664  tpr2rico  28726  qqhre  28832  indf1ofs  28855  eulerpartgbij  29213  eulerpartlemgh  29219  ballotlemscr  29359  ballotlemro  29363  ballotlemfrc  29367  ballotlemrinv0  29373  ballotlemscrOLD  29397  ballotlemroOLD  29401  ballotlemfrcOLD  29405  ballotlemrinv0OLD  29411  derangenlem  29902  subfacp1lem3  29913  subfacp1lem5  29915  erdsze2lem1  29934  cvmliftmolem1  30012  cvmlift2lem9a  30034  ghomf1olem  30320  phpreu  31893  poimirlem1  31905  poimirlem4  31908  poimirlem9  31913  poimirlem22  31926  mblfinlem2  31942  metf1o  32048  ismtyima  32099  ismtyres  32104  rngoisocnv  32184  laut11  33620  diaf1oN  34667  mapdcnvcl  35189  mapdcnvid2  35194  eldioph2lem2  35572  eldioph2  35573  pwfi2f1o  35924  gicabl  35927  sge0f1o  38132  nnfoctbdjlem  38201  usgrf1  39054  uspgr1  39100  usgrres1  39150  edgusgrnbfin  39211  usgrexi  39263  sizusglecusglem1  39279  usgresvm1  39375  usgresvm1ALT  39379
  Copyright terms: Public domain W3C validator