Theorem f1of1 6763

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

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

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 6489

This theorem is referenced by:  f1of  6764  f1un  6784  f1sng  6806  f1oresrab  7061  f1ounsn  7209  f1prex  7221  f1ocnvfvrneq  7223  f1ocoima  7240  isof1oidb  7261  isores3  7272  isoini2  7276  isosolem  7284  f1oiso  7288  weniso  7291  weisoeq  7292  f1opw2  7604  f1ovv  7893  mptcnfimad  7921  tposf12  8184  oacomf1olem  8482  enssdom  8902  domssex2  9054  mapen  9058  ssenen  9068  ssfiALT  9088  ssdomfi  9110  ssdomfi2  9111  sucdom2  9117  phplem2  9119  php3  9123  snnen2o  9134  1sdom2dom  9143  f1finf1o  9162  domunfican  9211  fiint  9216  fiintOLD  9217  f1opwfi  9246  mapfienlem1  9295  mapfienlem2  9296  mapfien  9298  marypha1lem  9323  ordtypelem10  9419  oiexg  9427  unxpwdom2  9480  wemapwe  9593  inlresf1  9811  inrresf1  9813  isinffi  9888  infxpenlem  9907  fseqenlem1  9918  dfac12lem2  10039  dfac12r  10041  ackbij2  10136  cff1  10152  infpssrlem4  10200  fin4en1  10203  enfin2i  10215  fin23lem28  10234  isf32lem7  10253  isf34lem3  10269  enfin1ai  10278  canthnum  10543  canthwe  10545  canthp1lem2  10547  pwfseqlem4  10556  pwfseqlem5  10557  tskuni  10677  grothomex  10723  negfi  12074  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  18651  injsubmefmnd  18771  xpsgrp  18938  eqgen  19060  conjsubgen  19130  subggim  19145  gim0to0  19148  gicsubgen  19158  symgfvne  19260  symgextf1  19300  symgfixelsi  19314  f1omvdmvd  19322  f1omvdconj  19325  pmtrfconj  19345  odngen  19456  sylow1lem2  19478  sylow2blem1  19499  gsumzres  19788  gsumzcl2  19789  gsumzf1o  19791  gsumzaddlem  19800  gsumconst  19813  gsumzmhm  19816  gsumzoppg  19823  dprdf1o  19913  xpsrngd  20064  xpsringd  20217  gsumfsum  21341  zntoslem  21463  znunithash  21471  iporthcom  21542  lindfres  21730  islindf3  21733  lindsmm  21735  lmimlbs  21743  lbslcic  21748  coe1sfi  22096  coe1mul2lem2  22152  resthauslem  23248  sshauslem  23257  basqtop  23596  tgqtop  23597  hmeoopn  23651  hmeocld  23652  hmeontr  23654  hmeoimaf1o  23655  haushmphlem  23672  tsmsf1o  24030  imasdsf1olem  24259  imasf1oxmet  24261  imasf1oxms  24375  ovoliunlem1  25401  dyadmbl  25499  vitalilem3  25509  dvcnvlem  25878  dvne0f1  25915  dvcnvrelem2  25921  logf1o2  26557  dvlog  26558  wilthlem3  26978  istrkg2ld  28405  f1otrg  28816  axcontlem10  28918  usgrf1  29117  usgrexmplef  29204  usgrres1  29260  edgusgrnbfin  29318  usgrexilem  29385  sizusglecusglem1  29407  uspgr2wlkeq  29591  trlres  29644  usgr2trlncl  29705  clwlkclwwlk  29946  adjbd1o  32029  padct  32662  indf1ofs  32809  s1f1  32884  s2f1  32886  mndlactf1o  32984  mndractf1o  32985  gsumwrd2dccat  33020  cycpmconjv  33084  1arithidomlem2  33473  mplvrpmfgalem  33545  mplvrpmga  33546  lmimdim  33570  madjusmdetlem4  33797  tpr2rico  33879  qqhre  33987  eulerpartgbij  34340  eulerpartlemgh  34346  ballotlemscr  34487  ballotlemro  34491  ballotlemfrc  34495  ballotlemrinv0  34501  reprpmtf1o  34594  onvf1od  35080  vonf1owev  35081  derangenlem  35144  subfacp1lem3  35155  subfacp1lem5  35157  erdsze2lem1  35176  cvmliftmolem1  35254  cvmlift2lem9a  35276  phpreu  37584  poimirlem1  37601  poimirlem4  37604  poimirlem9  37609  poimirlem22  37622  mblfinlem2  37638  metf1o  37735  ismtyima  37783  ismtyres  37788  rngoisocnv  37961  laut11  40065  diaf1oN  41109  mapdcnvcl  41631  mapdcnvid2  41636  ricdrng1  42501  evlselv  42560  eldioph2lem2  42734  eldioph2  42735  pwfi2f1o  43069  gicabl  43072  permaxext  44979  permac8prim  44988  sge0f1o  46363  nnfoctbdjlem  46436  3f1oss1  47059  f1ocof1ob2  47066  f1oresf1o  47274  fundcmpsurbijinjpreimafv  47391  fundcmpsurinjpreimafv  47392  fundcmpsurinjimaid  47395  grimcnv  47872  uhgrimedg  47875  isuspgrim0lem  47877  isuspgrim0  47878  isuspgrimlem  47879  upgrimtrlslem2  47889  upgrimpthslem2  47892  uhgrimisgrgriclem  47914  uhgrimisgrgric  47915  clnbgrgrimlem  47917  grimedg  47919  grtriproplem  47923  grtrif1o  47926  grimgrtri  47933  stgrusgra  47943  isubgr3stgrlem4  47953  isubgr3stgrlem7  47956  isubgr3stgrlem8  47957  grlimgrtri  47987  usgrexmpl1lem  48005  usgrexmpl2lem  48010  gpgusgra  48041  imaidfu  49095  uptrlem1  49195