Theorem f1of1 6771

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 6497	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
2	1	simplbi 497	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)

Syntax hints:   → wi 4  –1-1→wf1 6487  –onto→wfo 6488  –1-1-onto→wf1o 6489

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 207  df-an 396  df-f1o 6497

This theorem is referenced by:  f1of  6772  f1un  6792  f1sng  6815  f1oresrab  7070  f1ounsn  7216  f1prex  7228  f1ocnvfvrneq  7230  f1ocoima  7247  isof1oidb  7268  isores3  7279  isoini2  7283  isosolem  7291  f1oiso  7295  weniso  7298  weisoeq  7299  f1opw2  7611  f1ovv  7900  mptcnfimad  7928  tposf12  8191  oacomf1olem  8489  enssdom  8911  enssdomOLD  8912  domssex2  9063  mapen  9067  ssenen  9077  ssfiALT  9096  ssdomfi  9118  ssdomfi2  9119  sucdom2  9125  phplem2  9127  php3  9131  snnen2o  9143  1sdom2dom  9152  f1finf1o  9171  domunfican  9220  fiint  9225  f1opwfi  9254  mapfienlem1  9306  mapfienlem2  9307  mapfien  9309  marypha1lem  9334  ordtypelem10  9430  oiexg  9438  unxpwdom2  9491  wemapwe  9604  inlresf1  9825  inrresf1  9827  isinffi  9902  infxpenlem  9921  fseqenlem1  9932  dfac12lem2  10053  dfac12r  10055  ackbij2  10150  cff1  10166  infpssrlem4  10214  fin4en1  10217  enfin2i  10229  fin23lem28  10248  isf32lem7  10267  isf34lem3  10283  enfin1ai  10292  canthnum  10558  canthwe  10560  canthp1lem2  10562  pwfseqlem4  10571  pwfseqlem5  10572  tskuni  10692  grothomex  10738  negfi  12089  seqf1olem1  13962  hashfacen  14375  hashf1lem1  14376  fsumss  15646  ackbijnn  15749  fprodss  15869  bitsinv2  16368  bitsf1  16371  sadasslem  16395  sadeq  16397  phimullem  16704  eulerthlem2  16707  unbenlem  16834  f1ocpbllem  17443  f1ovscpbl  17445  xpsff1o2  17488  xpsmnd  18700  injsubmefmnd  18820  xpsgrp  18987  eqgen  19108  conjsubgen  19178  subggim  19193  gim0to0  19196  gicsubgen  19206  symgfvne  19308  symgextf1  19348  symgfixelsi  19362  f1omvdmvd  19370  f1omvdconj  19373  pmtrfconj  19393  odngen  19504  sylow1lem2  19526  sylow2blem1  19547  gsumzres  19836  gsumzcl2  19837  gsumzf1o  19839  gsumzaddlem  19848  gsumconst  19861  gsumzmhm  19864  gsumzoppg  19871  dprdf1o  19961  xpsrngd  20112  xpsringd  20266  gsumfsum  21387  zntoslem  21509  znunithash  21517  iporthcom  21588  lindfres  21776  islindf3  21779  lindsmm  21781  lmimlbs  21789  lbslcic  21794  coe1sfi  22152  coe1mul2lem2  22208  resthauslem  23305  sshauslem  23314  basqtop  23653  tgqtop  23654  hmeoopn  23708  hmeocld  23709  hmeontr  23711  hmeoimaf1o  23712  haushmphlem  23729  tsmsf1o  24087  imasdsf1olem  24315  imasf1oxmet  24317  imasf1oxms  24431  ovoliunlem1  25457  dyadmbl  25555  vitalilem3  25565  dvcnvlem  25934  dvne0f1  25971  dvcnvrelem2  25977  logf1o2  26613  dvlog  26614  wilthlem3  27034  oldfib  28335  istrkg2ld  28481  f1otrg  28892  axcontlem10  28995  usgrf1  29194  usgrexmplef  29281  usgrres1  29337  edgusgrnbfin  29395  usgrexilem  29462  sizusglecusglem1  29484  uspgr2wlkeq  29668  trlres  29721  usgr2trlncl  29782  clwlkclwwlk  30026  adjbd1o  32109  padct  32746  indf1ofs  32897  s1f1  32974  s2f1  32976  mndlactf1o  33061  mndractf1o  33062  gsumwrd2dccat  33109  cycpmconjv  33173  1arithidomlem2  33566  mplvrpmlem  33657  mplvrpmfgalem  33658  mplvrpmga  33659  mplvrpmmhm  33660  mplvrpmrhm  33661  esplysply  33678  lmimdim  33709  madjusmdetlem4  33936  tpr2rico  34018  qqhre  34126  eulerpartgbij  34478  eulerpartlemgh  34484  ballotlemscr  34625  ballotlemro  34629  ballotlemfrc  34633  ballotlemrinv0  34639  reprpmtf1o  34732  onvf1od  35250  vonf1owev  35251  derangenlem  35314  subfacp1lem3  35325  subfacp1lem5  35327  erdsze2lem1  35346  cvmliftmolem1  35424  cvmlift2lem9a  35446  phpreu  37744  poimirlem1  37761  poimirlem4  37764  poimirlem9  37769  poimirlem22  37782  mblfinlem2  37798  metf1o  37895  ismtyima  37943  ismtyres  37948  rngoisocnv  38121  laut11  40285  diaf1oN  41329  mapdcnvcl  41851  mapdcnvid2  41856  ricdrng1  42725  evlselv  42772  eldioph2lem2  42945  eldioph2  42946  pwfi2f1o  43280  gicabl  43283  permaxext  45188  permac8prim  45197  sge0f1o  46568  nnfoctbdjlem  46641  3f1oss1  47263  f1ocof1ob2  47270  f1oresf1o  47478  fundcmpsurbijinjpreimafv  47595  fundcmpsurinjpreimafv  47596  fundcmpsurinjimaid  47599  grimcnv  48076  uhgrimedg  48079  isuspgrim0lem  48081  isuspgrim0  48082  isuspgrimlem  48083  upgrimtrlslem2  48093  upgrimpthslem2  48096  uhgrimisgrgriclem  48118  uhgrimisgrgric  48119  clnbgrgrimlem  48121  grimedg  48123  grtriproplem  48127  grtrif1o  48130  grimgrtri  48137  stgrusgra  48147  isubgr3stgrlem4  48157  isubgr3stgrlem7  48160  isubgr3stgrlem8  48161  grlimgrtri  48191  usgrexmpl1lem  48209  usgrexmpl2lem  48214  gpgusgra  48245  imaidfu  49297  uptrlem1  49397