Theorem f1of1 6845

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

Syntax hints:   → wi 4  –1-1→wf1 6556  –onto→wfo 6557  –1-1-onto→wf1o 6558

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 6566

This theorem is referenced by:  f1of  6846  f1un  6866  f1sng  6888  f1oresrab  7145  f1ounsn  7290  f1prex  7302  f1ocnvfvrneq  7304  f1ocoima  7321  isof1oidb  7342  isores3  7353  isoini2  7357  isosolem  7365  f1oiso  7369  weniso  7372  weisoeq  7373  f1opw2  7685  f1ovv  7978  mptcnfimad  8007  tposf12  8272  oacomf1olem  8598  enssdom  9013  sucdom2OLD  9118  domssex2  9173  mapen  9177  ssenen  9187  ssfiALT  9210  ssdomfi  9232  ssdomfi2  9233  sucdom2  9239  phplem2  9241  php3  9245  phplem4OLD  9253  php3OLD  9257  snnen2o  9269  1sdom2dom  9279  f1finf1o  9301  f1finf1oOLD  9302  domunfican  9357  fiint  9362  fiintOLD  9363  f1opwfi  9392  mapfienlem1  9441  mapfienlem2  9442  mapfien  9444  marypha1lem  9469  ordtypelem10  9563  oiexg  9571  unxpwdom2  9624  wemapwe  9733  inlresf1  9951  inrresf1  9953  isinffi  10028  infxpenlem  10049  fseqenlem1  10060  dfac12lem2  10181  dfac12r  10183  ackbij2  10278  cff1  10294  infpssrlem4  10342  fin4en1  10345  enfin2i  10357  fin23lem28  10376  isf32lem7  10395  isf34lem3  10411  enfin1ai  10420  canthnum  10685  canthwe  10687  canthp1lem2  10689  pwfseqlem4  10698  pwfseqlem5  10699  tskuni  10819  grothomex  10865  negfi  12213  seqf1olem1  14078  hashfacen  14489  hashf1lem1  14490  fsumss  15757  ackbijnn  15860  fprodss  15980  bitsinv2  16476  bitsf1  16479  sadasslem  16503  sadeq  16505  phimullem  16812  eulerthlem2  16815  unbenlem  16942  f1ocpbllem  17565  f1ovscpbl  17567  xpsff1o2  17610  xpsmnd  18786  injsubmefmnd  18906  xpsgrp  19073  eqgen  19195  conjsubgen  19265  subggim  19280  gim0to0  19283  gicsubgen  19293  symgfvne  19394  symgextf1  19435  symgfixelsi  19449  f1omvdmvd  19457  f1omvdconj  19460  pmtrfconj  19480  odngen  19591  sylow1lem2  19613  sylow2blem1  19634  gsumzres  19923  gsumzcl2  19924  gsumzf1o  19926  gsumzaddlem  19935  gsumconst  19948  gsumzmhm  19951  gsumzoppg  19958  dprdf1o  20048  xpsrngd  20172  xpsringd  20321  gsumfsum  21444  zntoslem  21567  znunithash  21575  iporthcom  21645  lindfres  21835  islindf3  21838  lindsmm  21840  lmimlbs  21848  lbslcic  21853  coe1sfi  22205  coe1mul2lem2  22261  resthauslem  23361  sshauslem  23370  basqtop  23709  tgqtop  23710  hmeoopn  23764  hmeocld  23765  hmeontr  23767  hmeoimaf1o  23768  haushmphlem  23785  tsmsf1o  24143  imasdsf1olem  24373  imasf1oxmet  24375  imasf1oxms  24492  ovoliunlem1  25527  dyadmbl  25625  vitalilem3  25635  dvcnvlem  26004  dvne0f1  26041  dvcnvrelem2  26047  logf1o2  26682  dvlog  26683  wilthlem3  27103  istrkg2ld  28458  f1otrg  28869  axcontlem10  28978  usgrf1  29179  usgrexmplef  29266  usgrres1  29322  edgusgrnbfin  29380  usgrexilem  29447  sizusglecusglem1  29469  uspgr2wlkeq  29654  trlres  29708  usgr2trlncl  29770  clwlkclwwlk  30011  adjbd1o  32094  padct  32720  indf1ofs  32838  s1f1  32914  s2f1  32916  mndlactf1o  33020  mndractf1o  33021  gsumwrd2dccat  33055  cycpmconjv  33147  1arithidomlem2  33551  lmimdim  33641  madjusmdetlem4  33807  tpr2rico  33889  qqhre  33999  eulerpartgbij  34352  eulerpartlemgh  34358  ballotlemscr  34499  ballotlemro  34503  ballotlemfrc  34507  ballotlemrinv0  34513  reprpmtf1o  34619  derangenlem  35154  subfacp1lem3  35165  subfacp1lem5  35167  erdsze2lem1  35186  cvmliftmolem1  35264  cvmlift2lem9a  35286  phpreu  37589  poimirlem1  37606  poimirlem4  37609  poimirlem9  37614  poimirlem22  37627  mblfinlem2  37643  metf1o  37740  ismtyima  37788  ismtyres  37793  rngoisocnv  37966  laut11  40066  diaf1oN  41110  mapdcnvcl  41632  mapdcnvid2  41637  ricdrng1  42516  evlselv  42575  eldioph2lem2  42750  eldioph2  42751  pwfi2f1o  43086  gicabl  43089  sge0f1o  46370  nnfoctbdjlem  46443  3f1oss1  47060  f1ocof1ob2  47067  f1oresf1o  47275  fundcmpsurbijinjpreimafv  47367  fundcmpsurinjpreimafv  47368  fundcmpsurinjimaid  47371  isuspgrim0lem  47844  isuspgrim0  47845  uspgrimprop  47846  isuspgrimlem  47847  grimcnv  47852  uhgrimisgrgriclem  47871  uhgrimisgrgric  47872  clnbgrgrimlem  47874  grimedg  47876  grtriproplem  47879  grtrif1o  47882  grimgrtri  47889  stgrusgra  47899  isubgr3stgrlem4  47909  isubgr3stgrlem7  47912  isubgr3stgrlem8  47913  grlimgrtri  47936  usgrexmpl1lem  47953  usgrexmpl2lem  47958  gpgusgra  47985