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

Theorem f1of1 5840
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 5612 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
21simplbi 466 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 5602   -onto->wfo 5603   -1-1-onto->wf1o 5604
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 190  df-an 377  df-f1o 5612
This theorem is referenced by:  f1of  5841  f1oresrab  6084  f1prex  6212  f1ocnvfvrneq  6214  isores3  6256  isoini2  6260  isosolem  6268  f1oiso  6272  weniso  6275  weisoeq  6276  f1opw2  6554  f1ovv  6796  tposf12  7029  oacomf1olem  7296  enssdom  7625  domssex2  7763  mapen  7767  ssenen  7777  phplem4  7785  php3  7789  sucdom2  7799  ssfi  7823  f1finf1o  7829  domunfican  7875  fiint  7879  f1opwfi  7909  mapfienlem1  7949  mapfienlem2  7950  mapfien  7952  marypha1lem  7978  ordtypelem10  8073  oiexg  8081  unxpwdom2  8134  wemapwe  8233  isinffi  8457  infxpenlem  8475  fseqenlem1  8486  dfac12lem2  8605  dfac12r  8607  ackbij2  8704  cff1  8719  infpssrlem4  8767  fin4en1  8770  enfin2i  8782  fin23lem28  8801  isf32lem7  8820  isf34lem3  8836  enfin1ai  8845  canthnum  9105  canthwe  9107  canthp1lem2  9109  pwfseqlem4  9118  pwfseqlem5  9119  tskuni  9239  grothomex  9285  negfi  10587  seqf1olem1  12290  hashfacen  12656  hashf1lem1  12657  fsumss  13846  ackbijnn  13941  fprodss  14057  bitsinv2  14472  bitsf1  14475  sadasslem  14499  sadeq  14501  phimullem  14782  eulerthlem2  14785  unbenlem  14907  f1ocpbllem  15485  f1ovscpbl  15487  xpsff1o2  15532  xpsmnd  16631  xpsgrp  16860  eqgen  16925  conjsubgen  16970  subggim  16985  gicsubgen  16997  symgfvne  17084  symgextf1  17117  symgfixelsi  17131  f1omvdmvd  17139  f1omvdconj  17142  pmtrfconj  17162  odngen  17281  sylow1lem2  17306  sylow2blem1  17327  gsumzres  17598  gsumzcl2  17599  gsumzf1o  17601  gsumzaddlem  17609  gsumconst  17622  gsumzmhm  17625  gsumzoppg  17632  dprdf1o  17720  rim0to0  18025  coe1sfi  18861  coe1mul2lem2  18916  gsumfsum  19089  zntoslem  19182  znunithash  19190  iporthcom  19257  lindfres  19436  islindf3  19439  lindsmm  19441  lmimlbs  19449  lbslcic  19454  resthauslem  20434  sshauslem  20443  basqtop  20781  tgqtop  20782  hmeoopn  20836  hmeocld  20837  hmeontr  20839  hmeoimaf1o  20840  haushmphlem  20857  tsmsf1o  21214  imasdsf1olem  21443  imasf1oxmet  21445  imasf1oxms  21559  ovoliunlem1  22510  dyadmbl  22614  vitalilem3  22624  dvcnvlem  22984  dvne0f1  23020  dvcnvrelem2  23026  logf1o2  23651  dvlog  23652  wilthlem3  24051  istrkg2ld  24564  f1otrg  24957  axcontlem10  25059  usgraf1  25143  uslgra1  25155  usgra1  25156  usgraexmplef  25184  edgusgranbfin  25234  cusgraexilem2  25251  sizeusglecusglem1  25268  2trllemE  25339  constr1trl  25374  usgra2adedgspthlem2  25396  constr3trllem2  25435  eupatrl  25752  eupares  25759  eupath2lem3  25763  adjbd1o  27794  padct  28359  madjusmdetlem4  28707  tpr2rico  28769  qqhre  28875  indf1ofs  28898  eulerpartgbij  29255  eulerpartlemgh  29261  ballotlemscr  29401  ballotlemro  29405  ballotlemfrc  29409  ballotlemrinv0  29415  ballotlemscrOLD  29439  ballotlemroOLD  29443  ballotlemfrcOLD  29447  ballotlemrinv0OLD  29453  derangenlem  29944  subfacp1lem3  29955  subfacp1lem5  29957  erdsze2lem1  29976  cvmliftmolem1  30054  cvmlift2lem9a  30076  ghomf1olem  30362  phpreu  31975  poimirlem1  31987  poimirlem4  31990  poimirlem9  31995  poimirlem22  32008  mblfinlem2  32024  metf1o  32130  ismtyima  32181  ismtyres  32186  rngoisocnv  32266  laut11  33697  diaf1oN  34744  mapdcnvcl  35266  mapdcnvid2  35271  eldioph2lem2  35649  eldioph2  35650  pwfi2f1o  36000  gicabl  36003  sge0f1o  38327  nnfoctbdjlem  38398  usgrf1  39403  uspgr1e  39465  usgrres1  39528  edgusgrnbfin  39593  usgrexi  39652  sizusglecusglem1  39668  usgresvm1  40124  usgresvm1ALT  40128
  Copyright terms: Public domain W3C validator