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  18686  injsubmefmnd  18806  xpsgrp  18973  eqgen  19095  conjsubgen  19165  subggim  19180  gim0to0  19183  gicsubgen  19193  symgfvne  19295  symgextf1  19335  symgfixelsi  19349  f1omvdmvd  19357  f1omvdconj  19360  pmtrfconj  19380  odngen  19491  sylow1lem2  19513  sylow2blem1  19534  gsumzres  19823  gsumzcl2  19824  gsumzf1o  19826  gsumzaddlem  19835  gsumconst  19848  gsumzmhm  19851  gsumzoppg  19858  dprdf1o  19948  xpsrngd  20099  xpsringd  20252  gsumfsum  21376  zntoslem  21498  znunithash  21506  iporthcom  21577  lindfres  21765  islindf3  21768  lindsmm  21770  lmimlbs  21778  lbslcic  21783  coe1sfi  22131  coe1mul2lem2  22187  resthauslem  23283  sshauslem  23292  basqtop  23631  tgqtop  23632  hmeoopn  23686  hmeocld  23687  hmeontr  23689  hmeoimaf1o  23690  haushmphlem  23707  tsmsf1o  24065  imasdsf1olem  24294  imasf1oxmet  24296  imasf1oxms  24410  ovoliunlem1  25436  dyadmbl  25534  vitalilem3  25544  dvcnvlem  25913  dvne0f1  25950  dvcnvrelem2  25956  logf1o2  26592  dvlog  26593  wilthlem3  27013  istrkg2ld  28440  f1otrg  28851  axcontlem10  28953  usgrf1  29152  usgrexmplef  29239  usgrres1  29295  edgusgrnbfin  29353  usgrexilem  29420  sizusglecusglem1  29442  uspgr2wlkeq  29626  trlres  29679  usgr2trlncl  29740  clwlkclwwlk  29981  adjbd1o  32064  padct  32693  indf1ofs  32839  s1f1  32914  s2f1  32916  mndlactf1o  33014  mndractf1o  33015  gsumwrd2dccat  33050  cycpmconjv  33114  1arithidomlem2  33500  lmimdim  33592  madjusmdetlem4  33813  tpr2rico  33895  qqhre  34003  eulerpartgbij  34356  eulerpartlemgh  34362  ballotlemscr  34503  ballotlemro  34507  ballotlemfrc  34511  ballotlemrinv0  34517  reprpmtf1o  34610  onvf1od  35087  vonf1owev  35088  derangenlem  35151  subfacp1lem3  35162  subfacp1lem5  35164  erdsze2lem1  35183  cvmliftmolem1  35261  cvmlift2lem9a  35283  phpreu  37591  poimirlem1  37608  poimirlem4  37611  poimirlem9  37616  poimirlem22  37629  mblfinlem2  37645  metf1o  37742  ismtyima  37790  ismtyres  37795  rngoisocnv  37968  laut11  40073  diaf1oN  41117  mapdcnvcl  41639  mapdcnvid2  41644  ricdrng1  42509  evlselv  42568  eldioph2lem2  42742  eldioph2  42743  pwfi2f1o  43078  gicabl  43081  permaxext  44988  permac8prim  44997  sge0f1o  46373  nnfoctbdjlem  46446  3f1oss1  47069  f1ocof1ob2  47076  f1oresf1o  47284  fundcmpsurbijinjpreimafv  47401  fundcmpsurinjpreimafv  47402  fundcmpsurinjimaid  47405  grimcnv  47881  uhgrimedg  47884  isuspgrim0lem  47886  isuspgrim0  47887  isuspgrimlem  47888  upgrimtrlslem2  47898  upgrimpthslem2  47901  uhgrimisgrgriclem  47923  uhgrimisgrgric  47924  clnbgrgrimlem  47926  grimedg  47928  grtriproplem  47931  grtrif1o  47934  grimgrtri  47941  stgrusgra  47951  isubgr3stgrlem4  47961  isubgr3stgrlem7  47964  isubgr3stgrlem8  47965  grlimgrtri  47988  usgrexmpl1lem  48005  usgrexmpl2lem  48010  gpgusgra  48041  imaidfu  49092  uptrlem1  49192