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

Theorem f1of1 6783
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 6503 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
21simplbi 498 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  1-1wf1 6493  ontowfo 6494  1-1-ontowf1o 6495
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 206  df-an 397  df-f1o 6503
This theorem is referenced by:  f1of  6784  f1un  6804  f1sng  6826  f1oresrab  7072  f1prex  7229  f1ocnvfvrneq  7231  isof1oidb  7268  isores3  7279  isoini2  7283  isosolem  7291  f1oiso  7295  weniso  7298  weisoeq  7299  f1opw2  7607  f1ovv  7889  tposf12  8181  oacomf1olem  8510  enssdom  8916  sucdom2OLD  9025  domssex2  9080  mapen  9084  ssenen  9094  ssfiALT  9117  ssdomfi  9142  ssdomfi2  9143  sucdom2  9149  phplem2  9151  php3  9155  phplem4OLD  9163  php3OLD  9167  snnen2o  9180  1sdom2dom  9190  f1finf1o  9214  f1finf1oOLD  9215  domunfican  9263  fiint  9267  f1opwfi  9299  mapfienlem1  9340  mapfienlem2  9341  mapfien  9343  marypha1lem  9368  ordtypelem10  9462  oiexg  9470  unxpwdom2  9523  wemapwe  9632  inlresf1  9850  inrresf1  9852  isinffi  9927  infxpenlem  9948  fseqenlem1  9959  dfac12lem2  10079  dfac12r  10081  ackbij2  10178  cff1  10193  infpssrlem4  10241  fin4en1  10244  enfin2i  10256  fin23lem28  10275  isf32lem7  10294  isf34lem3  10310  enfin1ai  10319  canthnum  10584  canthwe  10586  canthp1lem2  10588  pwfseqlem4  10597  pwfseqlem5  10598  tskuni  10718  grothomex  10764  negfi  12103  seqf1olem1  13946  hashfacen  14350  hashfacenOLD  14351  hashf1lem1  14352  hashf1lem1OLD  14353  fsumss  15609  ackbijnn  15712  fprodss  15830  bitsinv2  16322  bitsf1  16325  sadasslem  16349  sadeq  16351  phimullem  16650  eulerthlem2  16653  unbenlem  16779  f1ocpbllem  17405  f1ovscpbl  17407  xpsff1o2  17450  xpsmnd  18595  injsubmefmnd  18706  xpsgrp  18864  eqgen  18981  conjsubgen  19039  subggim  19054  gicsubgen  19066  symgfvne  19160  symgextf1  19201  symgfixelsi  19215  f1omvdmvd  19223  f1omvdconj  19226  pmtrfconj  19246  odngen  19357  sylow1lem2  19379  sylow2blem1  19400  gsumzres  19684  gsumzcl2  19685  gsumzf1o  19687  gsumzaddlem  19696  gsumconst  19709  gsumzmhm  19712  gsumzoppg  19719  dprdf1o  19809  gim0to0  20174  gsumfsum  20862  zntoslem  20961  znunithash  20969  iporthcom  21037  lindfres  21227  islindf3  21230  lindsmm  21232  lmimlbs  21240  lbslcic  21245  coe1sfi  21582  coe1mul2lem2  21637  resthauslem  22712  sshauslem  22721  basqtop  23060  tgqtop  23061  hmeoopn  23115  hmeocld  23116  hmeontr  23118  hmeoimaf1o  23119  haushmphlem  23136  tsmsf1o  23494  imasdsf1olem  23724  imasf1oxmet  23726  imasf1oxms  23843  ovoliunlem1  24864  dyadmbl  24962  vitalilem3  24972  dvcnvlem  25338  dvne0f1  25374  dvcnvrelem2  25380  logf1o2  26003  dvlog  26004  wilthlem3  26417  istrkg2ld  27349  f1otrg  27760  axcontlem10  27869  usgrf1  28070  usgrexmplef  28154  usgrres1  28210  edgusgrnbfin  28268  usgrexilem  28335  sizusglecusglem1  28356  uspgr2wlkeq  28541  trlres  28595  usgr2trlncl  28655  clwlkclwwlk  28893  adjbd1o  30974  padct  31580  s1f1  31743  s2f1  31745  cycpmconjv  31935  madjusmdetlem4  32351  tpr2rico  32433  qqhre  32541  indf1ofs  32565  eulerpartgbij  32912  eulerpartlemgh  32918  ballotlemscr  33058  ballotlemro  33062  ballotlemfrc  33066  ballotlemrinv0  33072  reprpmtf1o  33179  derangenlem  33705  subfacp1lem3  33716  subfacp1lem5  33718  erdsze2lem1  33737  cvmliftmolem1  33815  cvmlift2lem9a  33837  phpreu  36052  poimirlem1  36069  poimirlem4  36072  poimirlem9  36077  poimirlem22  36090  mblfinlem2  36106  metf1o  36204  ismtyima  36252  ismtyres  36257  rngoisocnv  36430  laut11  38539  diaf1oN  39583  mapdcnvcl  40105  mapdcnvid2  40110  eldioph2lem2  41061  eldioph2  41062  pwfi2f1o  41400  gicabl  41403  sge0f1o  44594  nnfoctbdjlem  44667  f1ocof1ob2  45285  f1oresf1o  45493  fundcmpsurbijinjpreimafv  45570  fundcmpsurinjpreimafv  45571  fundcmpsurinjimaid  45574  isomuspgrlem1  45990  isomuspgrlem2c  45993  isomgrsym  45999
  Copyright terms: Public domain W3C validator