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

Theorem f1of1 5664
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 5452 . 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 5442   -onto->wfo 5443   -1-1-onto->wf1o 5444
This theorem is referenced by:  f1of  5665  f1ocnvfvrneq  6010  isores3  6046  isoini2  6050  isosolem  6058  f1oiso  6062  weniso  6066  weisoeq  6067  f1opw2  6289  tposf12  6495  oacomf1olem  6798  enssdom  7123  domssex2  7258  mapen  7262  ssenen  7272  phplem4  7280  php3  7284  sucdom2  7294  ssfi  7320  f1finf1o  7326  domunfican  7370  fiint  7374  f1opwfi  7401  marypha1lem  7429  ordtypelem10  7485  oiexg  7493  unxpwdom2  7545  mapfien  7642  wemapwe  7643  isinffi  7868  infxpenlem  7884  fseqenlem1  7894  dfac12lem2  8013  dfac12r  8015  ackbij2  8112  cff1  8127  infpssrlem4  8175  fin4en1  8178  enfin2i  8190  fin23lem28  8209  isf32lem7  8228  isf34lem3  8244  enfin1ai  8253  canthnum  8513  canthwe  8515  canthp1lem2  8517  pwfseqlem4  8526  pwfseqlem5  8527  tskuni  8647  grothomex  8693  seqf1olem1  11350  hashfacen  11691  hashf1lem1  11692  fsumss  12507  ackbijnn  12595  bitsinv2  12943  bitsf1  12946  sadasslem  12970  sadeq  12972  phimullem  13156  eulerthlem2  13159  unbenlem  13264  f1ocpbllem  13737  f1ovscpbl  13739  xpsff1o2  13784  xpsmnd  14723  xpsgrp  14925  eqgen  14981  conjsubgen  15026  subggim  15041  gicsubgen  15053  odngen  15199  sylow1lem2  15221  sylow2blem1  15242  gsumzres  15505  gsumzcl  15506  gsumzf1o  15507  gsumzaddlem  15514  gsumconst  15520  gsumzmhm  15521  gsumzoppg  15527  dprdf1o  15578  coe1sfi  16598  coe1mul2lem2  16649  gsumfsum  16754  zntoslem  16825  znunithash  16833  iporthcom  16854  resthauslem  17415  sshauslem  17424  basqtop  17731  tgqtop  17732  hmeoopn  17786  hmeocld  17787  hmeontr  17789  hmeoimaf1o  17790  haushmphlem  17807  tsmsf1o  18162  imasdsf1olem  18391  imasf1oxmet  18393  imasf1oxms  18507  ovoliunlem1  19386  dyadmbl  19480  vitalilem3  19490  dvcnvlem  19848  dvne0f1  19884  dvcnvrelem2  19890  logf1o2  20529  dvlog  20530  wilthlem3  20841  usgraf1  21371  uslgra1  21380  usgra1  21381  usgraexmpl  21408  edgusgranbfin  21447  cusgraexilem2  21464  sizeusglecusglem1  21481  2trllemE  21541  constr1trl  21576  constr3trllem2  21626  eupatrl  21678  eupares  21685  eupath2lem3  21689  adjbd1o  23576  tpr2rico  24298  qqhre  24374  indf1ofs  24411  ballotlemscr  24764  ballotlemro  24768  ballotlemfrc  24772  ballotlemrinv0  24778  derangenlem  24845  subfacp1lem3  24856  subfacp1lem5  24858  erdsze2lem1  24877  cvmliftmolem1  24956  cvmlift2lem9a  24978  ghomf1olem  25093  fprodss  25263  axcontlem10  25860  mblfinlem  26190  metf1o  26398  ismtyima  26449  ismtyres  26454  rngoisocnv  26534  eldioph2lem2  26756  eldioph2  26757  pwfi2f1o  27175  gicabl  27178  lindfres  27208  islindf3  27211  lindsmm  27213  lmimlbs  27221  lbslcic  27226  f1omvdmvd  27301  f1omvdconj  27304  pmtrfconj  27322  usgra2adedgspthlem2  28188  laut11  30722  diaf1oN  31767  mapdcnvcl  32289  mapdcnvid2  32294
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 5452
  Copyright terms: Public domain W3C validator