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

Theorem f1of1 6318
Description: A one-to-one onto mapping is a one-to-one mapping. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1of1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)

Proof of Theorem f1of1
StepHypRef Expression
1 df-f1o 6074 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
21simplbi 491 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  1-1wf1 6064  ontowfo 6065  1-1-ontowf1o 6066
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 198  df-an 385  df-f1o 6074
This theorem is referenced by:  f1of  6319  f1sng  6360  f1oresrab  6584  f1prex  6730  f1ocnvfvrneq  6732  isof1oidb  6765  isores3  6776  isoini2  6780  isosolem  6788  f1oiso  6792  weniso  6795  weisoeq  6796  f1opw2  7085  f1ovv  7334  tposf12  7579  oacomf1olem  7848  enssdom  8184  domssex2  8326  mapen  8330  ssenen  8340  phplem4  8348  php3  8352  sucdom2  8362  ssfi  8386  f1finf1o  8393  domunfican  8439  fiint  8443  f1opwfi  8476  mapfienlem1  8516  mapfienlem2  8517  mapfien  8519  marypha1lem  8545  ordtypelem10  8638  oiexg  8646  unxpwdom2  8699  wemapwe  8808  inlresf1  8991  inrresf1  8993  isinffi  9068  infxpenlem  9086  fseqenlem1  9097  dfac12lem2  9218  dfac12r  9220  ackbij2  9317  cff1  9332  infpssrlem4  9380  fin4en1  9383  enfin2i  9395  fin23lem28  9414  isf32lem7  9433  isf34lem3  9449  enfin1ai  9458  canthnum  9723  canthwe  9725  canthp1lem2  9727  pwfseqlem4  9736  pwfseqlem5  9737  tskuni  9857  grothomex  9903  negfi  11224  seqf1olem1  13046  hashfacen  13438  hashf1lem1  13439  fsumss  14742  ackbijnn  14845  fprodss  14962  bitsinv2  15447  bitsf1  15450  sadasslem  15474  sadeq  15476  phimullem  15764  eulerthlem2  15767  unbenlem  15892  f1ocpbllem  16451  f1ovscpbl  16453  xpsff1o2  16498  xpsmnd  17597  xpsgrp  17802  eqgen  17912  conjsubgen  17958  subggim  17973  gicsubgen  17985  symgfvne  18072  symgextf1  18105  symgfixelsi  18119  f1omvdmvd  18127  f1omvdconj  18130  pmtrfconj  18150  odngen  18257  sylow1lem2  18279  sylow2blem1  18300  gsumzres  18575  gsumzcl2  18576  gsumzf1o  18578  gsumzaddlem  18586  gsumconst  18599  gsumzmhm  18602  gsumzoppg  18609  dprdf1o  18697  rim0to0  19010  coe1sfi  19855  coe1mul2lem2  19910  gsumfsum  20085  zntoslem  20176  znunithash  20184  iporthcom  20254  lindfres  20437  islindf3  20440  lindsmm  20442  lmimlbs  20450  lbslcic  20455  resthauslem  21446  sshauslem  21455  basqtop  21793  tgqtop  21794  hmeoopn  21848  hmeocld  21849  hmeontr  21851  hmeoimaf1o  21852  haushmphlem  21869  tsmsf1o  22226  imasdsf1olem  22456  imasf1oxmet  22458  imasf1oxms  22572  ovoliunlem1  23559  dyadmbl  23657  vitalilem3  23667  dvcnvlem  24029  dvne0f1  24065  dvcnvrelem2  24071  logf1o2  24686  dvlog  24687  wilthlem3  25086  istrkg2ld  25649  f1otrg  26041  axcontlem10  26143  usgrf1  26344  usgrexmplef  26429  usgrres1  26485  edgusgrnbfin  26553  usgrexilem  26626  sizusglecusglem1  26647  uspgr2wlkeq  26832  trlres  26887  usgr2trlncl  26946  clwlkclwwlk  27207  adjbd1o  29334  padct  29880  madjusmdetlem4  30277  tpr2rico  30339  qqhre  30445  indf1ofs  30469  eulerpartgbij  30815  eulerpartlemgh  30821  ballotlemscr  30962  ballotlemro  30966  ballotlemfrc  30970  ballotlemrinv0  30976  reprpmtf1o  31086  derangenlem  31532  subfacp1lem3  31543  subfacp1lem5  31545  erdsze2lem1  31564  cvmliftmolem1  31642  cvmlift2lem9a  31664  phpreu  33749  poimirlem1  33766  poimirlem4  33769  poimirlem9  33774  poimirlem22  33787  mblfinlem2  33803  metf1o  33905  ismtyima  33956  ismtyres  33961  rngoisocnv  34134  laut11  35974  diaf1oN  37018  mapdcnvcl  37540  mapdcnvid2  37545  eldioph2lem2  37934  eldioph2  37935  pwfi2f1o  38275  gicabl  38278  sge0f1o  41168  nnfoctbdjlem  41241  f1oresf1o  41971  f1oresf1o2  41972
  Copyright terms: Public domain W3C validator