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

Theorem f1of1 5830
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 5608 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
21simplbi 461 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 5598   -onto->wfo 5599   -1-1-onto->wf1o 5600
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 188  df-an 372  df-f1o 5608
This theorem is referenced by:  f1of  5831  f1oresrab  6070  f1prex  6197  f1ocnvfvrneq  6199  isores3  6241  isoini2  6245  isosolem  6253  f1oiso  6257  weniso  6260  weisoeq  6261  f1opw2  6536  f1ovv  6778  tposf12  7006  oacomf1olem  7273  enssdom  7601  domssex2  7738  mapen  7742  ssenen  7752  phplem4  7760  php3  7764  sucdom2  7774  ssfi  7798  f1finf1o  7804  domunfican  7850  fiint  7854  f1opwfi  7884  mapfienlem1  7924  mapfienlem2  7925  mapfien  7927  marypha1lem  7953  ordtypelem10  8042  oiexg  8050  unxpwdom2  8103  wemapwe  8201  isinffi  8425  infxpenlem  8443  fseqenlem1  8453  dfac12lem2  8572  dfac12r  8574  ackbij2  8671  cff1  8686  infpssrlem4  8734  fin4en1  8737  enfin2i  8749  fin23lem28  8768  isf32lem7  8787  isf34lem3  8803  enfin1ai  8812  canthnum  9073  canthwe  9075  canthp1lem2  9077  pwfseqlem4  9086  pwfseqlem5  9087  tskuni  9207  grothomex  9253  negfi  10554  seqf1olem1  12249  hashfacen  12612  hashf1lem1  12613  fsumss  13769  ackbijnn  13864  fprodss  13980  bitsinv2  14391  bitsf1  14394  sadasslem  14418  sadeq  14420  phimullem  14687  eulerthlem2  14690  unbenlem  14806  f1ocpbllem  15372  f1ovscpbl  15374  xpsff1o2  15419  xpsmnd  16518  xpsgrp  16747  eqgen  16812  conjsubgen  16857  subggim  16872  gicsubgen  16884  symgfvne  16971  symgextf1  17004  symgfixelsi  17018  f1omvdmvd  17026  f1omvdconj  17029  pmtrfconj  17049  odngen  17155  sylow1lem2  17177  sylow2blem1  17198  gsumzres  17469  gsumzcl2  17470  gsumzf1o  17472  gsumzaddlem  17480  gsumconst  17493  gsumzmhm  17496  gsumzoppg  17503  dprdf1o  17591  rim0to0  17896  coe1sfi  18732  coe1mul2lem2  18787  gsumfsum  18960  zntoslem  19049  znunithash  19057  iporthcom  19124  lindfres  19303  islindf3  19306  lindsmm  19308  lmimlbs  19316  lbslcic  19321  resthauslem  20301  sshauslem  20310  basqtop  20648  tgqtop  20649  hmeoopn  20703  hmeocld  20704  hmeontr  20706  hmeoimaf1o  20707  haushmphlem  20724  tsmsf1o  21081  imasdsf1olem  21310  imasf1oxmet  21312  imasf1oxms  21426  ovoliunlem1  22324  dyadmbl  22426  vitalilem3  22436  dvcnvlem  22796  dvne0f1  22832  dvcnvrelem2  22838  logf1o2  23451  dvlog  23452  wilthlem3  23851  istrkg2ld  24362  f1otrg  24738  axcontlem10  24840  usgraf1  24924  uslgra1  24936  usgra1  24937  usgraexmpl  24965  edgusgranbfin  25014  cusgraexilem2  25031  sizeusglecusglem1  25048  2trllemE  25119  constr1trl  25154  usgra2adedgspthlem2  25176  constr3trllem2  25215  eupatrl  25532  eupares  25539  eupath2lem3  25543  adjbd1o  27564  padct  28141  madjusmdetlem4  28486  tpr2rico  28548  qqhre  28654  indf1ofs  28677  eulerpartgbij  29022  eulerpartlemgh  29028  ballotlemscr  29168  ballotlemro  29172  ballotlemfrc  29176  ballotlemrinv0  29182  derangenlem  29673  subfacp1lem3  29684  subfacp1lem5  29686  erdsze2lem1  29705  cvmliftmolem1  29783  cvmlift2lem9a  29805  ghomf1olem  30091  phpreu  31623  poimirlem1  31635  poimirlem4  31638  poimirlem9  31643  poimirlem22  31656  mblfinlem2  31672  metf1o  31778  ismtyima  31829  ismtyres  31834  rngoisocnv  31914  laut11  33350  diaf1oN  34397  mapdcnvcl  34919  mapdcnvid2  34924  eldioph2lem2  35302  eldioph2  35303  pwfi2f1o  35650  gicabl  35653  sge0f1o  37748  nnfoctbdjlem  37792  usgresvm1  38503  usgresvm1ALT  38507
  Copyright terms: Public domain W3C validator