Theorem f1of1 6805

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

Syntax hints:   → wi 4  –1-1→wf1 6518  –onto→wfo 6519  –1-1-onto→wf1o 6520

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 209  df-an 400  df-f1o 6528

This theorem is referenced by:  f1of  6806  f1un  6827  f1sng  6850  f1oresrab  7109  f1ounsn  7256  f1prex  7268  f1ocnvfvrneq  7270  f1ocoima  7287  isof1oidb  7308  isores3  7319  isoini2  7323  isosolem  7331  f1oiso  7335  weniso  7338  weisoeq  7339  f1opw2  7651  f1ovv  7939  mptcnfimad  7967  tposf12  8231  oacomf1olem  8533  enssdom  8957  enssdomOLD  8958  domssex2  9109  mapen  9113  ssenen  9123  ssfiALT  9142  ssdomfi  9164  ssdomfi2  9165  sucdom2  9171  phplem2  9173  php3  9177  snnen2o  9189  1sdom2dom  9198  f1finf1o  9217  domunfican  9266  fiint  9271  f1opwfi  9299  mapfienlem1  9351  mapfienlem2  9352  mapfien  9354  marypha1lem  9379  ordtypelem10  9475  oiexg  9483  unxpwdom2  9536  wemapwe  9652  inlresf1  9873  inrresf1  9875  isinffi  9950  infxpenlem  9969  fseqenlem1  9980  dfac12lem2  10101  dfac12r  10103  ackbij2  10198  cff1  10215  infpssrlem4  10263  fin4en1  10266  enfin2i  10278  fin23lem28  10297  isf32lem7  10316  isf34lem3  10332  enfin1ai  10341  canthnum  10607  canthwe  10609  canthp1lem2  10611  pwfseqlem4  10620  pwfseqlem5  10621  tskuni  10741  grothomex  10787  negfi  12141  seqf1olem1  14054  hashfacen  14467  hashf1lem1  14468  fsumss  15752  ackbijnn  15858  fprodss  15978  bitsinv2  16477  bitsf1  16480  sadasslem  16504  sadeq  16506  phimullem  16814  eulerthlem2  16817  unbenlem  16944  f1ocpbllem  17554  f1ovscpbl  17556  xpsff1o2  17599  xpsmnd  18811  injsubmefmnd  18931  xpsgrp  19101  eqgen  19222  conjsubgen  19291  subggim  19306  gim0to0  19309  gicsubgen  19319  symgfvne  19421  symgextf1  19461  symgfixelsi  19475  f1omvdmvd  19483  f1omvdconj  19486  pmtrfconj  19506  odngen  19617  sylow1lem2  19639  sylow2blem1  19660  gsumzres  19949  gsumzcl2  19950  gsumzf1o  19952  gsumzaddlem  19961  gsumconst  19974  gsumzmhm  19977  gsumzoppg  19984  dprdf1o  20074  xpsrngd  20225  xpsringd  20377  gsumfsum  21483  zntoslem  21605  znunithash  21613  iporthcom  21684  lindfres  21872  islindf3  21875  lindsmm  21877  lmimlbs  21885  lbslcic  21890  coe1sfi  22272  coe1mul2lem2  22328  resthauslem  23420  sshauslem  23429  basqtop  23768  tgqtop  23769  hmeoopn  23823  hmeocld  23824  hmeontr  23826  hmeoimaf1o  23827  haushmphlem  23844  tsmsf1o  24202  imasdsf1olem  24430  imasf1oxmet  24432  imasf1oxms  24546  ovoliunlem1  25561  dyadmbl  25659  vitalilem3  25669  dvcnvlem  26035  dvne0f1  26071  dvcnvrelem2  26077  logf1o2  26712  dvlog  26713  wilthlem3  27131  oldfib  28467  istrkg2ld  28626  f1otrg  29068  axcontlem10  29171  usgrf1  29370  usgrexmplef  29457  usgrres1  29513  edgusgrnbfin  29571  usgrexilem  29638  sizusglecusglem1  29659  uspgr2wlkeq  29843  trlres  29896  usgr2trlncl  29957  clwlkclwwlk  30201  adjbd1o  32285  padct  32917  indf1ofs  33041  s1f1  33118  s2f1  33120  mndlactf1o  33205  mndractf1o  33206  gsumwrd2dccat  33255  cycpmconjv  33319  1arithidomlem2  33729  mplvrpmlem  33837  mplvrpmfgalem  33838  mplvrpmga  33839  mplvrpmmhm  33840  mplvrpmrhm  33841  esplysply  33865  lmimdim  33898  madjusmdetlem4  34124  tpr2rico  34206  qqhre  34314  eulerpartgbij  34666  eulerpartlemgh  34672  ballotlemscr  34813  ballotlemro  34817  ballotlemfrc  34821  ballotlemrinv0  34827  reprpmtf1o  34917  onvf1od  35447  vonf1owev  35449  vonf1owevOLD  35450  vonf1oonf1  35454  derangenlem  35518  subfacp1lem3  35529  subfacp1lem5  35531  erdsze2lem1  35550  cvmliftmolem1  35628  cvmlift2lem9a  35650  phpreu  38100  poimirlem1  38117  poimirlem4  38120  poimirlem9  38125  poimirlem22  38138  mblfinlem2  38154  metf1o  38251  ismtyima  38299  ismtyres  38304  rngoisocnv  38477  laut11  40707  diaf1oN  41751  mapdcnvcl  42273  mapdcnvid2  42278  ricdrng1  43143  evlselv  43168  eldioph2lem2  43339  eldioph2  43340  pwfi2f1o  43670  gicabl  43673  permaxext  45578  permac8prim  45587  sge0f1o  46953  nnfoctbdjlem  47026  3f1oss1  47666  f1ocof1ob2  47673  f1oresf1o  47881  fundcmpsurbijinjpreimafv  48010  fundcmpsurinjpreimafv  48011  fundcmpsurinjimaid  48014  grimcnv  48507  uhgrimedg  48510  isuspgrim0lem  48512  isuspgrim0  48513  isuspgrimlem  48514  upgrimtrlslem2  48524  upgrimpthslem2  48527  uhgrimisgrgriclem  48549  uhgrimisgrgric  48550  clnbgrgrimlem  48552  grimedg  48554  grtriproplem  48558  grtrif1o  48561  grimgrtri  48568  stgrusgra  48578  isubgr3stgrlem4  48588  isubgr3stgrlem7  48591  isubgr3stgrlem8  48592  grlimgrtri  48622  usgrexmpl1lem  48640  usgrexmpl2lem  48645  gpgusgra  48676  imaidfu  49728  uptrlem1  49828