Theorem f1of1 6781

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

Syntax hints:   → wi 4  –1-1→wf1 6496  –onto→wfo 6497  –1-1-onto→wf1o 6498

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 6506

This theorem is referenced by:  f1of  6782  f1un  6802  f1sng  6824  f1oresrab  7081  f1ounsn  7229  f1prex  7241  f1ocnvfvrneq  7243  f1ocoima  7260  isof1oidb  7281  isores3  7292  isoini2  7296  isosolem  7304  f1oiso  7308  weniso  7311  weisoeq  7312  f1opw2  7624  f1ovv  7916  mptcnfimad  7944  tposf12  8207  oacomf1olem  8505  enssdom  8925  domssex2  9078  mapen  9082  ssenen  9092  ssfiALT  9115  ssdomfi  9137  ssdomfi2  9138  sucdom2  9144  phplem2  9146  php3  9150  snnen2o  9161  1sdom2dom  9170  f1finf1o  9192  f1finf1oOLD  9193  domunfican  9248  fiint  9253  fiintOLD  9254  f1opwfi  9283  mapfienlem1  9332  mapfienlem2  9333  mapfien  9335  marypha1lem  9360  ordtypelem10  9456  oiexg  9464  unxpwdom2  9517  wemapwe  9626  inlresf1  9844  inrresf1  9846  isinffi  9921  infxpenlem  9942  fseqenlem1  9953  dfac12lem2  10074  dfac12r  10076  ackbij2  10171  cff1  10187  infpssrlem4  10235  fin4en1  10238  enfin2i  10250  fin23lem28  10269  isf32lem7  10288  isf34lem3  10304  enfin1ai  10313  canthnum  10578  canthwe  10580  canthp1lem2  10582  pwfseqlem4  10591  pwfseqlem5  10592  tskuni  10712  grothomex  10758  negfi  12108  seqf1olem1  13982  hashfacen  14395  hashf1lem1  14396  fsumss  15667  ackbijnn  15770  fprodss  15890  bitsinv2  16389  bitsf1  16392  sadasslem  16416  sadeq  16418  phimullem  16725  eulerthlem2  16728  unbenlem  16855  f1ocpbllem  17463  f1ovscpbl  17465  xpsff1o2  17508  xpsmnd  18680  injsubmefmnd  18800  xpsgrp  18967  eqgen  19089  conjsubgen  19159  subggim  19174  gim0to0  19177  gicsubgen  19187  symgfvne  19287  symgextf1  19327  symgfixelsi  19341  f1omvdmvd  19349  f1omvdconj  19352  pmtrfconj  19372  odngen  19483  sylow1lem2  19505  sylow2blem1  19526  gsumzres  19815  gsumzcl2  19816  gsumzf1o  19818  gsumzaddlem  19827  gsumconst  19840  gsumzmhm  19843  gsumzoppg  19850  dprdf1o  19940  xpsrngd  20064  xpsringd  20217  gsumfsum  21327  zntoslem  21442  znunithash  21450  iporthcom  21520  lindfres  21708  islindf3  21711  lindsmm  21713  lmimlbs  21721  lbslcic  21726  coe1sfi  22074  coe1mul2lem2  22130  resthauslem  23226  sshauslem  23235  basqtop  23574  tgqtop  23575  hmeoopn  23629  hmeocld  23630  hmeontr  23632  hmeoimaf1o  23633  haushmphlem  23650  tsmsf1o  24008  imasdsf1olem  24237  imasf1oxmet  24239  imasf1oxms  24353  ovoliunlem1  25379  dyadmbl  25477  vitalilem3  25487  dvcnvlem  25856  dvne0f1  25893  dvcnvrelem2  25899  logf1o2  26535  dvlog  26536  wilthlem3  26956  istrkg2ld  28363  f1otrg  28774  axcontlem10  28876  usgrf1  29075  usgrexmplef  29162  usgrres1  29218  edgusgrnbfin  29276  usgrexilem  29343  sizusglecusglem1  29365  uspgr2wlkeq  29549  trlres  29602  usgr2trlncl  29663  clwlkclwwlk  29904  adjbd1o  31987  padct  32616  indf1ofs  32762  s1f1  32837  s2f1  32839  mndlactf1o  32944  mndractf1o  32945  gsumwrd2dccat  32980  cycpmconjv  33072  1arithidomlem2  33480  lmimdim  33572  madjusmdetlem4  33793  tpr2rico  33875  qqhre  33983  eulerpartgbij  34336  eulerpartlemgh  34342  ballotlemscr  34483  ballotlemro  34487  ballotlemfrc  34491  ballotlemrinv0  34497  reprpmtf1o  34590  onvf1od  35067  vonf1owev  35068  derangenlem  35131  subfacp1lem3  35142  subfacp1lem5  35144  erdsze2lem1  35163  cvmliftmolem1  35241  cvmlift2lem9a  35263  phpreu  37571  poimirlem1  37588  poimirlem4  37591  poimirlem9  37596  poimirlem22  37609  mblfinlem2  37625  metf1o  37722  ismtyima  37770  ismtyres  37775  rngoisocnv  37948  laut11  40053  diaf1oN  41097  mapdcnvcl  41619  mapdcnvid2  41624  ricdrng1  42489  evlselv  42548  eldioph2lem2  42722  eldioph2  42723  pwfi2f1o  43058  gicabl  43061  permaxext  44968  permac8prim  44977  sge0f1o  46353  nnfoctbdjlem  46426  3f1oss1  47049  f1ocof1ob2  47056  f1oresf1o  47264  fundcmpsurbijinjpreimafv  47381  fundcmpsurinjpreimafv  47382  fundcmpsurinjimaid  47385  grimcnv  47861  uhgrimedg  47864  isuspgrim0lem  47866  isuspgrim0  47867  isuspgrimlem  47868  upgrimtrlslem2  47878  upgrimpthslem2  47881  uhgrimisgrgriclem  47903  uhgrimisgrgric  47904  clnbgrgrimlem  47906  grimedg  47908  grtriproplem  47911  grtrif1o  47914  grimgrtri  47921  stgrusgra  47931  isubgr3stgrlem4  47941  isubgr3stgrlem7  47944  isubgr3stgrlem8  47945  grlimgrtri  47968  usgrexmpl1lem  47985  usgrexmpl2lem  47990  gpgusgra  48021  imaidfu  49072  uptrlem1  49172