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

Theorem f1of1 6608
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 6356 . 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 6346  ontowfo 6347  1-1-ontowf1o 6348
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 208  df-an 397  df-f1o 6356
This theorem is referenced by:  f1of  6609  f1sng  6650  f1oresrab  6882  f1prex  7031  f1ocnvfvrneq  7033  isof1oidb  7066  isores3  7077  isoini2  7081  isosolem  7089  f1oiso  7093  weniso  7096  weisoeq  7097  f1opw2  7389  f1ovv  7650  tposf12  7908  oacomf1olem  8180  enssdom  8523  domssex2  8666  mapen  8670  ssenen  8680  phplem4  8688  php3  8692  sucdom2  8703  ssfi  8727  f1finf1o  8734  domunfican  8780  fiint  8784  f1opwfi  8817  mapfienlem1  8857  mapfienlem2  8858  mapfien  8860  marypha1lem  8886  ordtypelem10  8980  oiexg  8988  unxpwdom2  9041  wemapwe  9149  inlresf1  9333  inrresf1  9335  isinffi  9410  infxpenlem  9428  fseqenlem1  9439  dfac12lem2  9559  dfac12r  9561  ackbij2  9654  cff1  9669  infpssrlem4  9717  fin4en1  9720  enfin2i  9732  fin23lem28  9751  isf32lem7  9770  isf34lem3  9786  enfin1ai  9795  canthnum  10060  canthwe  10062  canthp1lem2  10064  pwfseqlem4  10073  pwfseqlem5  10074  tskuni  10194  grothomex  10240  negfi  11578  seqf1olem1  13399  hashfacen  13802  hashf1lem1  13803  fsumss  15072  ackbijnn  15173  fprodss  15292  bitsinv2  15782  bitsf1  15785  sadasslem  15809  sadeq  15811  phimullem  16106  eulerthlem2  16109  unbenlem  16234  f1ocpbllem  16787  f1ovscpbl  16789  xpsff1o2  16832  xpsmnd  17941  xpsgrp  18158  eqgen  18273  conjsubgen  18331  subggim  18346  gicsubgen  18358  symgfvne  18446  symgextf1  18480  symgfixelsi  18494  f1omvdmvd  18502  f1omvdconj  18505  pmtrfconj  18525  odngen  18633  sylow1lem2  18655  sylow2blem1  18676  gsumzres  18960  gsumzcl2  18961  gsumzf1o  18963  gsumzaddlem  18972  gsumconst  18985  gsumzmhm  18988  gsumzoppg  18995  dprdf1o  19085  gim0to0  19426  rim0to0OLD  19427  coe1sfi  20311  coe1mul2lem2  20366  gsumfsum  20542  zntoslem  20633  znunithash  20641  iporthcom  20709  lindfres  20897  islindf3  20900  lindsmm  20902  lmimlbs  20910  lbslcic  20915  resthauslem  21901  sshauslem  21910  basqtop  22249  tgqtop  22250  hmeoopn  22304  hmeocld  22305  hmeontr  22307  hmeoimaf1o  22308  haushmphlem  22325  tsmsf1o  22682  imasdsf1olem  22912  imasf1oxmet  22914  imasf1oxms  23028  ovoliunlem1  24032  dyadmbl  24130  vitalilem3  24140  dvcnvlem  24502  dvne0f1  24538  dvcnvrelem2  24544  logf1o2  25160  dvlog  25161  wilthlem3  25575  istrkg2ld  26174  f1otrg  26585  axcontlem10  26687  usgrf1  26885  usgrexmplef  26969  usgrres1  27025  edgusgrnbfin  27083  usgrexilem  27150  sizusglecusglem1  27171  uspgr2wlkeq  27355  trlres  27410  usgr2trlncl  27469  clwlkclwwlk  27708  adjbd1o  29790  padct  30382  s1f1  30547  s2f1  30549  cycpmconjv  30712  madjusmdetlem4  30995  tpr2rico  31055  qqhre  31161  indf1ofs  31185  eulerpartgbij  31530  eulerpartlemgh  31536  ballotlemscr  31676  ballotlemro  31680  ballotlemfrc  31684  ballotlemrinv0  31690  reprpmtf1o  31797  derangenlem  32316  subfacp1lem3  32327  subfacp1lem5  32329  erdsze2lem1  32348  cvmliftmolem1  32426  cvmlift2lem9a  32448  phpreu  34758  poimirlem1  34775  poimirlem4  34778  poimirlem9  34783  poimirlem22  34796  mblfinlem2  34812  metf1o  34913  ismtyima  34964  ismtyres  34969  rngoisocnv  35142  laut11  37104  diaf1oN  38148  mapdcnvcl  38670  mapdcnvid2  38675  eldioph2lem2  39238  eldioph2  39239  pwfi2f1o  39576  gicabl  39579  sge0f1o  42545  nnfoctbdjlem  42618  f1oresf1o  43370  isomuspgrlem1  43839  isomuspgrlem2c  43842  isomgrsym  43848  injsubmefmnd  43964
  Copyright terms: Public domain W3C validator