Theorem f1of1 6762

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

Syntax hints:   → wi 4  –1-1→wf1 6478  –onto→wfo 6479  –1-1-onto→wf1o 6480

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 6488

This theorem is referenced by:  f1of  6763  f1un  6783  f1sng  6805  f1oresrab  7060  f1ounsn  7206  f1prex  7218  f1ocnvfvrneq  7220  f1ocoima  7237  isof1oidb  7258  isores3  7269  isoini2  7273  isosolem  7281  f1oiso  7285  weniso  7288  weisoeq  7289  f1opw2  7601  f1ovv  7890  mptcnfimad  7918  tposf12  8181  oacomf1olem  8479  enssdom  8899  domssex2  9050  mapen  9054  ssenen  9064  ssfiALT  9083  ssdomfi  9105  ssdomfi2  9106  sucdom2  9112  phplem2  9114  php3  9118  snnen2o  9129  1sdom2dom  9138  f1finf1o  9157  domunfican  9206  fiint  9211  f1opwfi  9240  mapfienlem1  9289  mapfienlem2  9290  mapfien  9292  marypha1lem  9317  ordtypelem10  9413  oiexg  9421  unxpwdom2  9474  wemapwe  9587  inlresf1  9808  inrresf1  9810  isinffi  9885  infxpenlem  9904  fseqenlem1  9915  dfac12lem2  10036  dfac12r  10038  ackbij2  10133  cff1  10149  infpssrlem4  10197  fin4en1  10200  enfin2i  10212  fin23lem28  10231  isf32lem7  10250  isf34lem3  10266  enfin1ai  10275  canthnum  10540  canthwe  10542  canthp1lem2  10544  pwfseqlem4  10553  pwfseqlem5  10554  tskuni  10674  grothomex  10720  negfi  12071  seqf1olem1  13948  hashfacen  14361  hashf1lem1  14362  fsumss  15632  ackbijnn  15735  fprodss  15855  bitsinv2  16354  bitsf1  16357  sadasslem  16381  sadeq  16383  phimullem  16690  eulerthlem2  16693  unbenlem  16820  f1ocpbllem  17428  f1ovscpbl  17430  xpsff1o2  17473  xpsmnd  18685  injsubmefmnd  18805  xpsgrp  18972  eqgen  19093  conjsubgen  19163  subggim  19178  gim0to0  19181  gicsubgen  19191  symgfvne  19293  symgextf1  19333  symgfixelsi  19347  f1omvdmvd  19355  f1omvdconj  19358  pmtrfconj  19378  odngen  19489  sylow1lem2  19511  sylow2blem1  19532  gsumzres  19821  gsumzcl2  19822  gsumzf1o  19824  gsumzaddlem  19833  gsumconst  19846  gsumzmhm  19849  gsumzoppg  19856  dprdf1o  19946  xpsrngd  20097  xpsringd  20250  gsumfsum  21371  zntoslem  21493  znunithash  21501  iporthcom  21572  lindfres  21760  islindf3  21763  lindsmm  21765  lmimlbs  21773  lbslcic  21778  coe1sfi  22126  coe1mul2lem2  22182  resthauslem  23278  sshauslem  23287  basqtop  23626  tgqtop  23627  hmeoopn  23681  hmeocld  23682  hmeontr  23684  hmeoimaf1o  23685  haushmphlem  23702  tsmsf1o  24060  imasdsf1olem  24288  imasf1oxmet  24290  imasf1oxms  24404  ovoliunlem1  25430  dyadmbl  25528  vitalilem3  25538  dvcnvlem  25907  dvne0f1  25944  dvcnvrelem2  25950  logf1o2  26586  dvlog  26587  wilthlem3  27007  istrkg2ld  28438  f1otrg  28849  axcontlem10  28951  usgrf1  29150  usgrexmplef  29237  usgrres1  29293  edgusgrnbfin  29351  usgrexilem  29418  sizusglecusglem1  29440  uspgr2wlkeq  29624  trlres  29677  usgr2trlncl  29738  clwlkclwwlk  29982  adjbd1o  32065  padct  32701  indf1ofs  32847  s1f1  32924  s2f1  32926  mndlactf1o  33011  mndractf1o  33012  gsumwrd2dccat  33047  cycpmconjv  33111  1arithidomlem2  33501  mplvrpmlem  33573  mplvrpmfgalem  33574  mplvrpmga  33575  mplvrpmmhm  33576  mplvrpmrhm  33577  esplysply  33592  lmimdim  33616  madjusmdetlem4  33843  tpr2rico  33925  qqhre  34033  eulerpartgbij  34385  eulerpartlemgh  34391  ballotlemscr  34532  ballotlemro  34536  ballotlemfrc  34540  ballotlemrinv0  34546  reprpmtf1o  34639  onvf1od  35151  vonf1owev  35152  derangenlem  35215  subfacp1lem3  35226  subfacp1lem5  35228  erdsze2lem1  35247  cvmliftmolem1  35325  cvmlift2lem9a  35347  phpreu  37652  poimirlem1  37669  poimirlem4  37672  poimirlem9  37677  poimirlem22  37690  mblfinlem2  37706  metf1o  37803  ismtyima  37851  ismtyres  37856  rngoisocnv  38029  laut11  40133  diaf1oN  41177  mapdcnvcl  41699  mapdcnvid2  41704  ricdrng1  42569  evlselv  42628  eldioph2lem2  42802  eldioph2  42803  pwfi2f1o  43137  gicabl  43140  permaxext  45046  permac8prim  45055  sge0f1o  46428  nnfoctbdjlem  46501  3f1oss1  47114  f1ocof1ob2  47121  f1oresf1o  47329  fundcmpsurbijinjpreimafv  47446  fundcmpsurinjpreimafv  47447  fundcmpsurinjimaid  47450  grimcnv  47927  uhgrimedg  47930  isuspgrim0lem  47932  isuspgrim0  47933  isuspgrimlem  47934  upgrimtrlslem2  47944  upgrimpthslem2  47947  uhgrimisgrgriclem  47969  uhgrimisgrgric  47970  clnbgrgrimlem  47972  grimedg  47974  grtriproplem  47978  grtrif1o  47981  grimgrtri  47988  stgrusgra  47998  isubgr3stgrlem4  48008  isubgr3stgrlem7  48011  isubgr3stgrlem8  48012  grlimgrtri  48042  usgrexmpl1lem  48060  usgrexmpl2lem  48065  gpgusgra  48096  imaidfu  49150  uptrlem1  49250