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

Theorem f1of1 6103
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 5864 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
21simplbi 476 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  1-1wf1 5854  ontowfo 5855  1-1-ontowf1o 5856
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 197  df-an 386  df-f1o 5864
This theorem is referenced by:  f1of  6104  f1sng  6145  f1oresrab  6361  f1prex  6504  f1ocnvfvrneq  6506  isof1oidb  6539  isores3  6550  isoini2  6554  isosolem  6562  f1oiso  6566  weniso  6569  weisoeq  6570  f1opw2  6853  f1ovv  7099  tposf12  7337  oacomf1olem  7604  enssdom  7940  domssex2  8080  mapen  8084  ssenen  8094  phplem4  8102  php3  8106  sucdom2  8116  ssfi  8140  f1finf1o  8147  domunfican  8193  fiint  8197  f1opwfi  8230  mapfienlem1  8270  mapfienlem2  8271  mapfien  8273  marypha1lem  8299  ordtypelem10  8392  oiexg  8400  unxpwdom2  8453  wemapwe  8554  isinffi  8778  infxpenlem  8796  fseqenlem1  8807  dfac12lem2  8926  dfac12r  8928  ackbij2  9025  cff1  9040  infpssrlem4  9088  fin4en1  9091  enfin2i  9103  fin23lem28  9122  isf32lem7  9141  isf34lem3  9157  enfin1ai  9166  canthnum  9431  canthwe  9433  canthp1lem2  9435  pwfseqlem4  9444  pwfseqlem5  9445  tskuni  9565  grothomex  9611  negfi  10931  seqf1olem1  12796  hashfacen  13192  hashf1lem1  13193  fsumss  14405  ackbijnn  14504  fprodss  14622  bitsinv2  15108  bitsf1  15111  sadasslem  15135  sadeq  15137  phimullem  15427  eulerthlem2  15430  unbenlem  15555  f1ocpbllem  16124  f1ovscpbl  16126  xpsff1o2  16171  xpsmnd  17270  xpsgrp  17474  eqgen  17587  conjsubgen  17633  subggim  17648  gicsubgen  17661  symgfvne  17748  symgextf1  17781  symgfixelsi  17795  f1omvdmvd  17803  f1omvdconj  17806  pmtrfconj  17826  odngen  17932  sylow1lem2  17954  sylow2blem1  17975  gsumzres  18250  gsumzcl2  18251  gsumzf1o  18253  gsumzaddlem  18261  gsumconst  18274  gsumzmhm  18277  gsumzoppg  18284  dprdf1o  18371  rim0to0  18682  coe1sfi  19523  coe1mul2lem2  19578  gsumfsum  19753  zntoslem  19845  znunithash  19853  iporthcom  19920  lindfres  20102  islindf3  20105  lindsmm  20107  lmimlbs  20115  lbslcic  20120  resthauslem  21107  sshauslem  21116  basqtop  21454  tgqtop  21455  hmeoopn  21509  hmeocld  21510  hmeontr  21512  hmeoimaf1o  21513  haushmphlem  21530  tsmsf1o  21888  imasdsf1olem  22118  imasf1oxmet  22120  imasf1oxms  22234  ovoliunlem1  23210  dyadmbl  23308  vitalilem3  23319  dvcnvlem  23677  dvne0f1  23713  dvcnvrelem2  23719  logf1o2  24330  dvlog  24331  wilthlem3  24730  istrkg2ld  25293  f1otrg  25685  axcontlem10  25787  usgrf1  25994  usgrexmplef  26078  usgrres1  26129  edgusgrnbfin  26196  usgrexilem  26257  sizusglecusglem1  26278  uspgr2wlkeq  26445  trlres  26500  usgr2trlncl  26559  clwlkclwwlk  26804  adjbd1o  28832  padct  29381  madjusmdetlem4  29720  tpr2rico  29782  qqhre  29888  indf1ofs  29911  eulerpartgbij  30257  eulerpartlemgh  30263  ballotlemscr  30403  ballotlemro  30407  ballotlemfrc  30411  ballotlemrinv0  30417  derangenlem  30914  subfacp1lem3  30925  subfacp1lem5  30927  erdsze2lem1  30946  cvmliftmolem1  31024  cvmlift2lem9a  31046  phpreu  33064  poimirlem1  33081  poimirlem4  33084  poimirlem9  33089  poimirlem22  33102  mblfinlem2  33118  metf1o  33222  ismtyima  33273  ismtyres  33278  rngoisocnv  33451  laut11  34891  diaf1oN  35938  mapdcnvcl  36460  mapdcnvid2  36465  eldioph2lem2  36843  eldioph2  36844  pwfi2f1o  37185  gicabl  37188  sge0f1o  39936  nnfoctbdjlem  40009
  Copyright terms: Public domain W3C validator