Theorem f1of1 6766

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

Syntax hints:   → wi 4  –1-1→wf1 6482  –onto→wfo 6483  –1-1-onto→wf1o 6484

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 208  df-an 397  df-f1o 6492

This theorem is referenced by:  f1of  6767  f1un  6787  f1sng  6810  f1oresrab  7069  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  8913  enssdomOLD  8914  domssex2  9065  mapen  9069  ssenen  9079  ssfiALT  9098  ssdomfi  9120  ssdomfi2  9121  sucdom2  9127  phplem2  9129  php3  9133  snnen2o  9145  1sdom2dom  9154  f1finf1o  9173  domunfican  9222  fiint  9227  f1opwfi  9256  mapfienlem1  9308  mapfienlem2  9309  mapfien  9311  marypha1lem  9336  ordtypelem10  9432  oiexg  9440  unxpwdom2  9493  wemapwe  9609  inlresf1  9830  inrresf1  9832  isinffi  9907  infxpenlem  9926  fseqenlem1  9937  dfac12lem2  10058  dfac12r  10060  ackbij2  10155  cff1  10171  infpssrlem4  10219  fin4en1  10222  enfin2i  10234  fin23lem28  10253  isf32lem7  10272  isf34lem3  10288  enfin1ai  10297  canthnum  10563  canthwe  10565  canthp1lem2  10567  pwfseqlem4  10576  pwfseqlem5  10577  tskuni  10697  grothomex  10743  negfi  12096  seqf1olem1  13994  hashfacen  14407  hashf1lem1  14408  fsumss  15678  ackbijnn  15784  fprodss  15904  bitsinv2  16403  bitsf1  16406  sadasslem  16430  sadeq  16432  phimullem  16740  eulerthlem2  16743  unbenlem  16870  f1ocpbllem  17479  f1ovscpbl  17481  xpsff1o2  17524  xpsmnd  18736  injsubmefmnd  18856  xpsgrp  19026  eqgen  19147  conjsubgen  19217  subggim  19232  gim0to0  19235  gicsubgen  19245  symgfvne  19347  symgextf1  19387  symgfixelsi  19401  f1omvdmvd  19409  f1omvdconj  19412  pmtrfconj  19432  odngen  19543  sylow1lem2  19565  sylow2blem1  19586  gsumzres  19875  gsumzcl2  19876  gsumzf1o  19878  gsumzaddlem  19887  gsumconst  19900  gsumzmhm  19903  gsumzoppg  19910  dprdf1o  20000  xpsrngd  20151  xpsringd  20303  gsumfsum  21409  zntoslem  21531  znunithash  21539  iporthcom  21610  lindfres  21798  islindf3  21801  lindsmm  21803  lmimlbs  21811  lbslcic  21816  coe1sfi  22198  coe1mul2lem2  22254  resthauslem  23346  sshauslem  23355  basqtop  23694  tgqtop  23695  hmeoopn  23749  hmeocld  23750  hmeontr  23752  hmeoimaf1o  23753  haushmphlem  23770  tsmsf1o  24128  imasdsf1olem  24356  imasf1oxmet  24358  imasf1oxms  24472  ovoliunlem1  25487  dyadmbl  25585  vitalilem3  25595  dvcnvlem  25961  dvne0f1  25997  dvcnvrelem2  26003  logf1o2  26632  dvlog  26633  wilthlem3  27051  oldfib  28387  istrkg2ld  28546  f1otrg  28957  axcontlem10  29060  usgrf1  29259  usgrexmplef  29346  usgrres1  29402  edgusgrnbfin  29460  usgrexilem  29527  sizusglecusglem1  29548  uspgr2wlkeq  29732  trlres  29785  usgr2trlncl  29846  clwlkclwwlk  30090  adjbd1o  32174  padct  32810  indf1ofs  32945  s1f1  33022  s2f1  33024  mndlactf1o  33109  mndractf1o  33110  gsumwrd2dccat  33159  cycpmconjv  33223  1arithidomlem2  33619  mplvrpmlem  33727  mplvrpmfgalem  33728  mplvrpmga  33729  mplvrpmmhm  33730  mplvrpmrhm  33731  esplysply  33755  lmimdim  33788  madjusmdetlem4  34014  tpr2rico  34096  qqhre  34204  eulerpartgbij  34556  eulerpartlemgh  34562  ballotlemscr  34703  ballotlemro  34707  ballotlemfrc  34711  ballotlemrinv0  34717  reprpmtf1o  34810  onvf1od  35335  vonf1owev  35336  derangenlem  35399  subfacp1lem3  35410  subfacp1lem5  35412  erdsze2lem1  35431  cvmliftmolem1  35509  cvmlift2lem9a  35531  phpreu  37971  poimirlem1  37988  poimirlem4  37991  poimirlem9  37996  poimirlem22  38009  mblfinlem2  38025  metf1o  38122  ismtyima  38170  ismtyres  38175  rngoisocnv  38348  laut11  40578  diaf1oN  41622  mapdcnvcl  42144  mapdcnvid2  42149  ricdrng1  43014  evlselv  43039  eldioph2lem2  43210  eldioph2  43211  pwfi2f1o  43541  gicabl  43544  permaxext  45449  permac8prim  45458  sge0f1o  46825  nnfoctbdjlem  46898  3f1oss1  47538  f1ocof1ob2  47545  f1oresf1o  47753  fundcmpsurbijinjpreimafv  47882  fundcmpsurinjpreimafv  47883  fundcmpsurinjimaid  47886  grimcnv  48379  uhgrimedg  48382  isuspgrim0lem  48384  isuspgrim0  48385  isuspgrimlem  48386  upgrimtrlslem2  48396  upgrimpthslem2  48399  uhgrimisgrgriclem  48421  uhgrimisgrgric  48422  clnbgrgrimlem  48424  grimedg  48426  grtriproplem  48430  grtrif1o  48433  grimgrtri  48440  stgrusgra  48450  isubgr3stgrlem4  48460  isubgr3stgrlem7  48463  isubgr3stgrlem8  48464  grlimgrtri  48494  usgrexmpl1lem  48512  usgrexmpl2lem  48517  gpgusgra  48548  imaidfu  49600  uptrlem1  49700