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

Theorem f1of1 6377
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 6130 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
21simplbi 493 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  1-1wf1 6120  ontowfo 6121  1-1-ontowf1o 6122
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 199  df-an 387  df-f1o 6130
This theorem is referenced by:  f1of  6378  f1sng  6419  f1oresrab  6644  f1prex  6794  f1ocnvfvrneq  6796  isof1oidb  6829  isores3  6840  isoini2  6844  isosolem  6852  f1oiso  6856  weniso  6859  weisoeq  6860  f1opw2  7148  f1ovv  7399  tposf12  7642  oacomf1olem  7911  enssdom  8247  domssex2  8389  mapen  8393  ssenen  8403  phplem4  8411  php3  8415  sucdom2  8425  ssfi  8449  f1finf1o  8456  domunfican  8502  fiint  8506  f1opwfi  8539  mapfienlem1  8579  mapfienlem2  8580  mapfien  8582  marypha1lem  8608  ordtypelem10  8701  oiexg  8709  unxpwdom2  8762  wemapwe  8871  inlresf1  9054  inrresf1  9056  isinffi  9131  infxpenlem  9149  fseqenlem1  9160  dfac12lem2  9281  dfac12r  9283  ackbij2  9380  cff1  9395  infpssrlem4  9443  fin4en1  9446  enfin2i  9458  fin23lem28  9477  isf32lem7  9496  isf34lem3  9512  enfin1ai  9521  canthnum  9786  canthwe  9788  canthp1lem2  9790  pwfseqlem4  9799  pwfseqlem5  9800  tskuni  9920  grothomex  9966  negfi  11301  seqf1olem1  13134  hashfacen  13527  hashf1lem1  13528  fsumss  14833  ackbijnn  14934  fprodss  15051  bitsinv2  15538  bitsf1  15541  sadasslem  15565  sadeq  15567  phimullem  15855  eulerthlem2  15858  unbenlem  15983  f1ocpbllem  16537  f1ovscpbl  16539  xpsff1o2  16584  xpsmnd  17683  xpsgrp  17888  eqgen  17998  conjsubgen  18044  subggim  18059  gicsubgen  18071  symgfvne  18158  symgextf1  18191  symgfixelsi  18205  f1omvdmvd  18213  f1omvdconj  18216  pmtrfconj  18236  odngen  18343  sylow1lem2  18365  sylow2blem1  18386  gsumzres  18663  gsumzcl2  18664  gsumzf1o  18666  gsumzaddlem  18674  gsumconst  18687  gsumzmhm  18690  gsumzoppg  18697  dprdf1o  18785  rim0to0  19098  coe1sfi  19943  coe1mul2lem2  19998  gsumfsum  20173  zntoslem  20264  znunithash  20272  iporthcom  20342  lindfres  20529  islindf3  20532  lindsmm  20534  lmimlbs  20542  lbslcic  20547  resthauslem  21538  sshauslem  21547  basqtop  21885  tgqtop  21886  hmeoopn  21940  hmeocld  21941  hmeontr  21943  hmeoimaf1o  21944  haushmphlem  21961  tsmsf1o  22318  imasdsf1olem  22548  imasf1oxmet  22550  imasf1oxms  22664  ovoliunlem1  23668  dyadmbl  23766  vitalilem3  23776  dvcnvlem  24138  dvne0f1  24174  dvcnvrelem2  24180  logf1o2  24795  dvlog  24796  wilthlem3  25209  istrkg2ld  25772  f1otrg  26170  axcontlem10  26272  usgrf1  26471  usgrexmplef  26556  usgrres1  26612  edgusgrnbfin  26671  usgrexilem  26738  sizusglecusglem1  26759  uspgr2wlkeq  26943  trlres  27001  trlresOLD  27003  usgr2trlncl  27062  clwlkclwwlk  27331  clwlkclwwlkOLD  27332  adjbd1o  29488  padct  30034  madjusmdetlem4  30430  tpr2rico  30492  qqhre  30598  indf1ofs  30622  eulerpartgbij  30968  eulerpartlemgh  30974  ballotlemscr  31115  ballotlemro  31119  ballotlemfrc  31123  ballotlemrinv0  31129  reprpmtf1o  31242  derangenlem  31688  subfacp1lem3  31699  subfacp1lem5  31701  erdsze2lem1  31720  cvmliftmolem1  31798  cvmlift2lem9a  31820  phpreu  33929  lindsadd  33939  poimirlem1  33947  poimirlem4  33950  poimirlem9  33955  poimirlem22  33968  mblfinlem2  33984  metf1o  34086  ismtyima  34137  ismtyres  34142  rngoisocnv  34315  laut11  36154  diaf1oN  37198  mapdcnvcl  37720  mapdcnvid2  37725  eldioph2lem2  38161  eldioph2  38162  pwfi2f1o  38502  gicabl  38505  sge0f1o  41383  nnfoctbdjlem  41456  f1oresf1o  42186  f1oresf1o2  42187  isomuspgrlem1  42538  isomuspgrlem2c  42541  isomgrsym  42547
  Copyright terms: Public domain W3C validator