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

Theorem f1of1 5821
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 5601 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
21simplbi 460 1  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   -1-1->wf1 5591   -onto->wfo 5592   -1-1-onto->wf1o 5593
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 185  df-an 371  df-f1o 5601
This theorem is referenced by:  f1of  5822  f1oresrab  6064  f1ocnvfvrneq  6188  isores3  6230  isoini2  6234  isosolem  6242  f1oiso  6246  weniso  6249  weisoeq  6250  f1opw2  6523  f1ovv  6766  tposf12  6992  oacomf1olem  7225  enssdom  7552  domssex2  7689  mapen  7693  ssenen  7703  phplem4  7711  php3  7715  sucdom2  7726  ssfi  7752  f1finf1o  7758  domunfican  7805  fiint  7809  f1opwfi  7836  mapfienlem1  7876  mapfienlem2  7877  mapfien  7879  marypha1lem  7905  ordtypelem10  7964  oiexg  7972  unxpwdom2  8026  mapfienOLD  8150  wemapwe  8151  wemapweOLD  8152  isinffi  8385  infxpenlem  8403  fseqenlem1  8417  dfac12lem2  8536  dfac12r  8538  ackbij2  8635  cff1  8650  infpssrlem4  8698  fin4en1  8701  enfin2i  8713  fin23lem28  8732  isf32lem7  8751  isf34lem3  8767  enfin1ai  8776  canthnum  9039  canthwe  9041  canthp1lem2  9043  pwfseqlem4  9052  pwfseqlem5  9053  tskuni  9173  grothomex  9219  seqf1olem1  12126  hashfacen  12483  hashf1lem1  12484  fsumss  13526  ackbijnn  13619  bitsinv2  13968  bitsf1  13971  sadasslem  13995  sadeq  13997  phimullem  14184  eulerthlem2  14187  unbenlem  14301  f1ocpbllem  14795  f1ovscpbl  14797  xpsff1o2  14842  xpsmnd  15832  xpsgrp  16060  eqgen  16125  conjsubgen  16170  subggim  16185  gicsubgen  16197  symgfvne  16284  symgextf1  16317  symgfixelsi  16331  f1omvdmvd  16339  f1omvdconj  16342  pmtrfconj  16362  odngen  16468  sylow1lem2  16490  sylow2blem1  16511  gsumzres  16785  gsumzcl2  16786  gsumzf1o  16788  gsumzresOLD  16789  gsumzclOLD  16790  gsumzf1oOLD  16791  gsumzaddlem  16805  gsumzaddlemOLD  16807  gsumconst  16825  gsumzmhm  16828  gsumzmhmOLD  16829  gsumzoppg  16838  gsumzoppgOLD  16839  dprdf1o  16949  rim0to0  17260  coe1sfi  18120  coe1sfiOLD  18121  coe1mul2lem2  18177  gsumfsum  18352  zntoslem  18462  znunithash  18470  iporthcom  18537  lindfres  18725  islindf3  18728  lindsmm  18730  lmimlbs  18738  lbslcic  18743  resthauslem  19730  sshauslem  19739  basqtop  20078  tgqtop  20079  hmeoopn  20133  hmeocld  20134  hmeontr  20136  hmeoimaf1o  20137  haushmphlem  20154  tsmsf1o  20513  imasdsf1olem  20742  imasf1oxmet  20744  imasf1oxms  20858  ovoliunlem1  21779  dyadmbl  21875  vitalilem3  21885  dvcnvlem  22243  dvne0f1  22279  dvcnvrelem2  22285  logf1o2  22895  dvlog  22896  wilthlem3  23208  istrkg2ld  23722  f1otrg  24006  axcontlem10  24108  usgraf1  24192  uslgra1  24204  usgra1  24205  usgraexmpl  24233  edgusgranbfin  24282  cusgraexilem2  24299  sizeusglecusglem1  24316  2trllemE  24387  constr1trl  24422  usgra2adedgspthlem2  24444  constr3trllem2  24483  eupatrl  24800  eupares  24807  eupath2lem3  24811  adjbd1o  26835  tpr2rico  27726  qqhre  27830  indf1ofs  27871  eulerpartgbij  28143  eulerpartlemgh  28149  ballotlemscr  28289  ballotlemro  28293  ballotlemfrc  28297  ballotlemrinv0  28303  derangenlem  28447  subfacp1lem3  28458  subfacp1lem5  28460  erdsze2lem1  28479  cvmliftmolem1  28558  cvmlift2lem9a  28580  ghomf1olem  28866  fprodss  29014  mblfinlem2  29986  metf1o  30182  ismtyima  30233  ismtyres  30238  rngoisocnv  30318  eldioph2lem2  30628  eldioph2  30629  pwfi2f1o  30978  gicabl  30981  usgresvm1  32239  usgresvm1ALT  32243  laut11  35288  diaf1oN  36333  mapdcnvcl  36855  mapdcnvid2  36860
  Copyright terms: Public domain W3C validator