Theorem f1of1 6724

Description: A one-to-one onto mapping is a one-to-one mapping. (Contributed by NM, 12-Dec-2003.)

Assertion

Ref	Expression
f1of1	⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)

Proof of Theorem f1of1

Step	Hyp	Ref	Expression
1		df-f1o 6444	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
2	1	simplbi 498	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)

Syntax hints:   → wi 4  –1-1→wf1 6434  –onto→wfo 6435  –1-1-onto→wf1o 6436

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 206  df-an 397  df-f1o 6444

This theorem is referenced by:  f1of  6725  f1un  6745  f1sng  6767  f1oresrab  7008  f1prex  7165  f1ocnvfvrneq  7167  isof1oidb  7204  isores3  7215  isoini2  7219  isosolem  7227  f1oiso  7231  weniso  7234  weisoeq  7235  f1opw2  7533  f1ovv  7809  tposf12  8076  oacomf1olem  8404  enssdom  8774  sucdom2OLD  8878  domssex2  8933  mapen  8937  ssenen  8947  ssfiALT  8966  ssdomfi  8991  ssdomfi2  8992  sucdom2  8998  phplem2  9000  php3  9004  phplem4OLD  9012  php3OLD  9016  snnen2o  9035  f1finf1o  9055  domunfican  9096  fiint  9100  f1opwfi  9132  mapfienlem1  9173  mapfienlem2  9174  mapfien  9176  marypha1lem  9201  ordtypelem10  9295  oiexg  9303  unxpwdom2  9356  wemapwe  9464  inlresf1  9682  inrresf1  9684  isinffi  9759  infxpenlem  9778  fseqenlem1  9789  dfac12lem2  9909  dfac12r  9911  ackbij2  10008  cff1  10023  infpssrlem4  10071  fin4en1  10074  enfin2i  10086  fin23lem28  10105  isf32lem7  10124  isf34lem3  10140  enfin1ai  10149  canthnum  10414  canthwe  10416  canthp1lem2  10418  pwfseqlem4  10427  pwfseqlem5  10428  tskuni  10548  grothomex  10594  negfi  11933  seqf1olem1  13771  hashfacen  14175  hashfacenOLD  14176  hashf1lem1  14177  hashf1lem1OLD  14178  fsumss  15446  ackbijnn  15549  fprodss  15667  bitsinv2  16159  bitsf1  16162  sadasslem  16186  sadeq  16188  phimullem  16489  eulerthlem2  16492  unbenlem  16618  f1ocpbllem  17244  f1ovscpbl  17246  xpsff1o2  17289  xpsmnd  18434  injsubmefmnd  18545  xpsgrp  18703  eqgen  18818  conjsubgen  18876  subggim  18891  gicsubgen  18903  symgfvne  18997  symgextf1  19038  symgfixelsi  19052  f1omvdmvd  19060  f1omvdconj  19063  pmtrfconj  19083  odngen  19191  sylow1lem2  19213  sylow2blem1  19234  gsumzres  19519  gsumzcl2  19520  gsumzf1o  19522  gsumzaddlem  19531  gsumconst  19544  gsumzmhm  19547  gsumzoppg  19554  dprdf1o  19644  gim0to0  19995  gsumfsum  20674  zntoslem  20773  znunithash  20781  iporthcom  20849  lindfres  21039  islindf3  21042  lindsmm  21044  lmimlbs  21052  lbslcic  21057  coe1sfi  21393  coe1mul2lem2  21448  resthauslem  22523  sshauslem  22532  basqtop  22871  tgqtop  22872  hmeoopn  22926  hmeocld  22927  hmeontr  22929  hmeoimaf1o  22930  haushmphlem  22947  tsmsf1o  23305  imasdsf1olem  23535  imasf1oxmet  23537  imasf1oxms  23654  ovoliunlem1  24675  dyadmbl  24773  vitalilem3  24783  dvcnvlem  25149  dvne0f1  25185  dvcnvrelem2  25191  logf1o2  25814  dvlog  25815  wilthlem3  26228  istrkg2ld  26830  f1otrg  27241  axcontlem10  27350  usgrf1  27551  usgrexmplef  27635  usgrres1  27691  edgusgrnbfin  27749  usgrexilem  27816  sizusglecusglem1  27837  uspgr2wlkeq  28022  trlres  28077  usgr2trlncl  28137  clwlkclwwlk  28375  adjbd1o  30456  padct  31063  s1f1  31226  s2f1  31228  cycpmconjv  31418  madjusmdetlem4  31789  tpr2rico  31871  qqhre  31979  indf1ofs  32003  eulerpartgbij  32348  eulerpartlemgh  32354  ballotlemscr  32494  ballotlemro  32498  ballotlemfrc  32502  ballotlemrinv0  32508  reprpmtf1o  32615  derangenlem  33142  subfacp1lem3  33153  subfacp1lem5  33155  erdsze2lem1  33174  cvmliftmolem1  33252  cvmlift2lem9a  33274  phpreu  35770  poimirlem1  35787  poimirlem4  35790  poimirlem9  35795  poimirlem22  35808  mblfinlem2  35824  metf1o  35922  ismtyima  35970  ismtyres  35975  rngoisocnv  36148  laut11  38107  diaf1oN  39151  mapdcnvcl  39673  mapdcnvid2  39678  eldioph2lem2  40590  eldioph2  40591  pwfi2f1o  40928  gicabl  40931  sge0f1o  43927  nnfoctbdjlem  44000  f1ocof1ob2  44585  f1oresf1o  44793  fundcmpsurbijinjpreimafv  44870  fundcmpsurinjpreimafv  44871  fundcmpsurinjimaid  44874  isomuspgrlem1  45290  isomuspgrlem2c  45293  isomgrsym  45299