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

Theorem f1of1 5487
Description: A one-to-one onto mapping is a one-to-one mapping. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1of1  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )

Proof of Theorem f1of1
StepHypRef Expression
1 df-f1o 5278 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
21simplbi 446 1  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   -1-1->wf1 5268   -onto->wfo 5269   -1-1-onto->wf1o 5270
This theorem is referenced by:  f1of  5488  isores3  5848  isoini2  5852  isosolem  5860  f1oiso  5864  weniso  5868  weisoeq  5869  f1opw2  6087  tposf12  6275  oacomf1olem  6578  enssdom  6902  domssex2  7037  mapen  7041  ssenen  7051  phplem4  7059  php3  7063  sucdom2  7073  ssfi  7099  f1finf1o  7102  domunfican  7145  fiint  7149  f1opwfi  7175  marypha1lem  7202  ordtypelem10  7258  oiexg  7266  unxpwdom2  7318  mapfien  7415  wemapwe  7416  isinffi  7641  infxpenlem  7657  fseqenlem1  7667  dfac12lem2  7786  dfac12r  7788  ackbij2  7885  cff1  7900  infpssrlem4  7948  fin4en1  7951  enfin2i  7963  fin23lem28  7982  isf32lem7  8001  isf34lem3  8017  enfin1ai  8026  canthnum  8287  canthwe  8289  canthp1lem2  8291  pwfseqlem4  8300  pwfseqlem5  8301  tskuni  8421  grothomex  8467  seqf1olem1  11101  hashfacen  11408  hashf1lem1  11409  fsumss  12214  ackbijnn  12302  bitsinv2  12650  bitsf1  12653  sadasslem  12677  sadeq  12679  phimullem  12863  eulerthlem2  12866  unbenlem  12971  f1ocpbllem  13442  f1ovscpbl  13444  xpsff1o2  13489  xpsmnd  14428  xpsgrp  14630  eqgen  14686  conjsubgen  14731  subggim  14746  gicsubgen  14758  odngen  14904  sylow1lem2  14926  sylow2blem1  14947  gsumzres  15210  gsumzcl  15211  gsumzf1o  15212  gsumzaddlem  15219  gsumconst  15225  gsumzmhm  15226  gsumzoppg  15232  dprdf1o  15283  coe1sfi  16309  coe1mul2lem2  16361  gsumfsum  16455  zntoslem  16526  znunithash  16534  iporthcom  16555  resthauslem  17107  sshauslem  17116  basqtop  17418  tgqtop  17419  hmeoopn  17473  hmeocld  17474  hmeontr  17476  hmeoimaf1o  17477  haushmphlem  17494  tsmsf1o  17843  imasdsf1olem  17953  imasf1oxmet  17955  imasf1oxms  18051  ovoliunlem1  18877  dyadmbl  18971  vitalilem3  18981  dvcnvlem  19339  dvne0f1  19375  dvcnvrelem2  19381  logf1o2  20013  dvlog  20014  wilthlem3  20324  adjbd1o  22681  ballotlemscr  23093  ballotlemro  23097  ballotlemfrc  23101  ballotlemrinv0  23107  tpr2rico  23311  indf1ofs  23624  derangenlem  23717  subfacp1lem3  23728  subfacp1lem5  23730  erdsze2lem1  23749  cvmliftmolem1  23827  cvmlift2lem9a  23849  eupares  23914  eupath2lem3  23918  ghomf1olem  24016  axcontlem10  24673  f2imacnv  25155  grpodlcan  25479  grpodivzer  25480  metf1o  26572  ismtyima  26630  ismtyres  26635  rngoisocnv  26715  eldioph2lem2  26943  eldioph2  26944  pwfi2f1o  27363  gicabl  27366  lindfres  27396  islindf3  27399  lindsmm  27401  lmimlbs  27409  lbslcic  27414  f1omvdmvd  27489  f1omvdconj  27492  pmtrfconj  27510  f1ocnvfvrneq  28189  usgraf1  28243  uslgra1  28252  usgra1  28253  usgraexmpl  28267  eupatrl  28385  constr3trllem2  28397  laut11  30897  diaf1oN  31942  mapdcnvcl  32464  mapdcnvid2  32469
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-f1o 5278
  Copyright terms: Public domain W3C validator