Theorem f1of1 6136

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

Step	Hyp	Ref	Expression
1		df-f1o 5895	. 2 |- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
2	1	simplbi 476	1 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )

Syntax hints:   -> wi 4   -1-1->wf1 5885   -onto->wfo 5886   -1-1-onto->wf1o 5887

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 197  df-an 386  df-f1o 5895

This theorem is referenced by:  f1of  6137  f1sng  6178  f1oresrab  6395  f1prex  6539  f1ocnvfvrneq  6541  isof1oidb  6574  isores3  6585  isoini2  6589  isosolem  6597  f1oiso  6601  weniso  6604  weisoeq  6605  f1opw2  6888  f1ovv  7137  tposf12  7377  oacomf1olem  7644  enssdom  7980  domssex2  8120  mapen  8124  ssenen  8134  phplem4  8142  php3  8146  sucdom2  8156  ssfi  8180  f1finf1o  8187  domunfican  8233  fiint  8237  f1opwfi  8270  mapfienlem1  8310  mapfienlem2  8311  mapfien  8313  marypha1lem  8339  ordtypelem10  8432  oiexg  8440  unxpwdom2  8493  wemapwe  8594  isinffi  8818  infxpenlem  8836  fseqenlem1  8847  dfac12lem2  8966  dfac12r  8968  ackbij2  9065  cff1  9080  infpssrlem4  9128  fin4en1  9131  enfin2i  9143  fin23lem28  9162  isf32lem7  9181  isf34lem3  9197  enfin1ai  9206  canthnum  9471  canthwe  9473  canthp1lem2  9475  pwfseqlem4  9484  pwfseqlem5  9485  tskuni  9605  grothomex  9651  negfi  10971  seqf1olem1  12840  hashfacen  13238  hashf1lem1  13239  fsumss  14456  ackbijnn  14560  fprodss  14678  bitsinv2  15165  bitsf1  15168  sadasslem  15192  sadeq  15194  phimullem  15484  eulerthlem2  15487  unbenlem  15612  f1ocpbllem  16184  f1ovscpbl  16186  xpsff1o2  16231  xpsmnd  17330  xpsgrp  17534  eqgen  17647  conjsubgen  17693  subggim  17708  gicsubgen  17721  symgfvne  17808  symgextf1  17841  symgfixelsi  17855  f1omvdmvd  17863  f1omvdconj  17866  pmtrfconj  17886  odngen  17992  sylow1lem2  18014  sylow2blem1  18035  gsumzres  18310  gsumzcl2  18311  gsumzf1o  18313  gsumzaddlem  18321  gsumconst  18334  gsumzmhm  18337  gsumzoppg  18344  dprdf1o  18431  rim0to0  18742  coe1sfi  19583  coe1mul2lem2  19638  gsumfsum  19813  zntoslem  19905  znunithash  19913  iporthcom  19980  lindfres  20162  islindf3  20165  lindsmm  20167  lmimlbs  20175  lbslcic  20180  resthauslem  21167  sshauslem  21176  basqtop  21514  tgqtop  21515  hmeoopn  21569  hmeocld  21570  hmeontr  21572  hmeoimaf1o  21573  haushmphlem  21590  tsmsf1o  21948  imasdsf1olem  22178  imasf1oxmet  22180  imasf1oxms  22294  ovoliunlem1  23270  dyadmbl  23368  vitalilem3  23379  dvcnvlem  23739  dvne0f1  23775  dvcnvrelem2  23781  logf1o2  24396  dvlog  24397  wilthlem3  24796  istrkg2ld  25359  f1otrg  25751  axcontlem10  25853  usgrf1  26067  usgrexmplef  26151  usgrres1  26207  edgusgrnbfin  26275  usgrexilem  26336  sizusglecusglem1  26357  uspgr2wlkeq  26542  trlres  26597  usgr2trlncl  26656  clwlkclwwlk  26903  adjbd1o  28944  padct  29497  madjusmdetlem4  29896  tpr2rico  29958  qqhre  30064  indf1ofs  30088  eulerpartgbij  30434  eulerpartlemgh  30440  ballotlemscr  30580  ballotlemro  30584  ballotlemfrc  30588  ballotlemrinv0  30594  reprpmtf1o  30704  derangenlem  31153  subfacp1lem3  31164  subfacp1lem5  31166  erdsze2lem1  31185  cvmliftmolem1  31263  cvmlift2lem9a  31285  phpreu  33393  poimirlem1  33410  poimirlem4  33413  poimirlem9  33418  poimirlem22  33431  mblfinlem2  33447  metf1o  33551  ismtyima  33602  ismtyres  33607  rngoisocnv  33780  laut11  35372  diaf1oN  36419  mapdcnvcl  36941  mapdcnvid2  36946  eldioph2lem2  37324  eldioph2  37325  pwfi2f1o  37666  gicabl  37669  sge0f1o  40599  nnfoctbdjlem  40672