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

Theorem f1of1 5673
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 5461 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
21simplbi 447 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 5451   -onto->wfo 5452   -1-1-onto->wf1o 5453
This theorem is referenced by:  f1of  5674  f1ocnvfvrneq  6019  isores3  6055  isoini2  6059  isosolem  6067  f1oiso  6071  weniso  6075  weisoeq  6076  f1opw2  6298  tposf12  6504  oacomf1olem  6807  enssdom  7132  domssex2  7267  mapen  7271  ssenen  7281  phplem4  7289  php3  7293  sucdom2  7303  ssfi  7329  f1finf1o  7335  domunfican  7379  fiint  7383  f1opwfi  7410  marypha1lem  7438  ordtypelem10  7496  oiexg  7504  unxpwdom2  7556  mapfien  7653  wemapwe  7654  isinffi  7879  infxpenlem  7895  fseqenlem1  7905  dfac12lem2  8024  dfac12r  8026  ackbij2  8123  cff1  8138  infpssrlem4  8186  fin4en1  8189  enfin2i  8201  fin23lem28  8220  isf32lem7  8239  isf34lem3  8255  enfin1ai  8264  canthnum  8524  canthwe  8526  canthp1lem2  8528  pwfseqlem4  8537  pwfseqlem5  8538  tskuni  8658  grothomex  8704  seqf1olem1  11362  hashfacen  11703  hashf1lem1  11704  fsumss  12519  ackbijnn  12607  bitsinv2  12955  bitsf1  12958  sadasslem  12982  sadeq  12984  phimullem  13168  eulerthlem2  13171  unbenlem  13276  f1ocpbllem  13749  f1ovscpbl  13751  xpsff1o2  13796  xpsmnd  14735  xpsgrp  14937  eqgen  14993  conjsubgen  15038  subggim  15053  gicsubgen  15065  odngen  15211  sylow1lem2  15233  sylow2blem1  15254  gsumzres  15517  gsumzcl  15518  gsumzf1o  15519  gsumzaddlem  15526  gsumconst  15532  gsumzmhm  15533  gsumzoppg  15539  dprdf1o  15590  coe1sfi  16610  coe1mul2lem2  16661  gsumfsum  16766  zntoslem  16837  znunithash  16845  iporthcom  16866  resthauslem  17427  sshauslem  17436  basqtop  17743  tgqtop  17744  hmeoopn  17798  hmeocld  17799  hmeontr  17801  hmeoimaf1o  17802  haushmphlem  17819  tsmsf1o  18174  imasdsf1olem  18403  imasf1oxmet  18405  imasf1oxms  18519  ovoliunlem1  19398  dyadmbl  19492  vitalilem3  19502  dvcnvlem  19860  dvne0f1  19896  dvcnvrelem2  19902  logf1o2  20541  dvlog  20542  wilthlem3  20853  usgraf1  21383  uslgra1  21392  usgra1  21393  usgraexmpl  21420  edgusgranbfin  21459  cusgraexilem2  21476  sizeusglecusglem1  21493  2trllemE  21553  constr1trl  21588  constr3trllem2  21638  eupatrl  21690  eupares  21697  eupath2lem3  21701  adjbd1o  23588  tpr2rico  24310  qqhre  24386  indf1ofs  24423  ballotlemscr  24776  ballotlemro  24780  ballotlemfrc  24784  ballotlemrinv0  24790  derangenlem  24857  subfacp1lem3  24868  subfacp1lem5  24870  erdsze2lem1  24889  cvmliftmolem1  24968  cvmlift2lem9a  24990  ghomf1olem  25105  fprodss  25274  axcontlem10  25912  mblfinlem2  26244  metf1o  26461  ismtyima  26512  ismtyres  26517  rngoisocnv  26597  eldioph2lem2  26819  eldioph2  26820  pwfi2f1o  27237  gicabl  27240  lindfres  27270  islindf3  27273  lindsmm  27275  lmimlbs  27283  lbslcic  27288  f1omvdmvd  27363  f1omvdconj  27366  pmtrfconj  27384  usgra2adedgspthlem2  28314  laut11  30883  diaf1oN  31928  mapdcnvcl  32450  mapdcnvid2  32455
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 178  df-an 361  df-f1o 5461
  Copyright terms: Public domain W3C validator