Theorem f1of1 6864

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

Syntax hints:   → wi 4  –1-1→wf1 6573  –onto→wfo 6574  –1-1-onto→wf1o 6575

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 6583

This theorem is referenced by:  f1of  6865  f1un  6885  f1sng  6907  f1oresrab  7164  f1prex  7323  f1ocnvfvrneq  7325  f1ocoima  7342  isof1oidb  7363  isores3  7374  isoini2  7378  isosolem  7386  f1oiso  7390  weniso  7393  weisoeq  7394  f1opw2  7708  f1ovv  8001  mptcnfimad  8030  tposf12  8295  oacomf1olem  8623  enssdom  9040  sucdom2OLD  9151  domssex2  9206  mapen  9210  ssenen  9220  ssfiALT  9244  ssdomfi  9265  ssdomfi2  9266  sucdom2  9272  phplem2  9274  php3  9278  phplem4OLD  9286  php3OLD  9290  snnen2o  9303  1sdom2dom  9313  f1finf1o  9336  f1finf1oOLD  9337  domunfican  9392  fiint  9397  fiintOLD  9398  f1opwfi  9429  mapfienlem1  9477  mapfienlem2  9478  mapfien  9480  marypha1lem  9505  ordtypelem10  9599  oiexg  9607  unxpwdom2  9660  wemapwe  9769  inlresf1  9987  inrresf1  9989  isinffi  10064  infxpenlem  10085  fseqenlem1  10096  dfac12lem2  10217  dfac12r  10219  ackbij2  10314  cff1  10330  infpssrlem4  10378  fin4en1  10381  enfin2i  10393  fin23lem28  10412  isf32lem7  10431  isf34lem3  10447  enfin1ai  10456  canthnum  10721  canthwe  10723  canthp1lem2  10725  pwfseqlem4  10734  pwfseqlem5  10735  tskuni  10855  grothomex  10901  negfi  12249  seqf1olem1  14109  hashfacen  14520  hashf1lem1  14521  fsumss  15790  ackbijnn  15893  fprodss  16013  bitsinv2  16509  bitsf1  16512  sadasslem  16536  sadeq  16538  phimullem  16846  eulerthlem2  16849  unbenlem  16975  f1ocpbllem  17604  f1ovscpbl  17606  xpsff1o2  17649  xpsmnd  18832  injsubmefmnd  18952  xpsgrp  19119  eqgen  19241  conjsubgen  19311  subggim  19326  gim0to0  19329  gicsubgen  19339  symgfvne  19442  symgextf1  19483  symgfixelsi  19497  f1omvdmvd  19505  f1omvdconj  19508  pmtrfconj  19528  odngen  19639  sylow1lem2  19661  sylow2blem1  19682  gsumzres  19971  gsumzcl2  19972  gsumzf1o  19974  gsumzaddlem  19983  gsumconst  19996  gsumzmhm  19999  gsumzoppg  20006  dprdf1o  20096  xpsrngd  20226  xpsringd  20375  gsumfsum  21495  zntoslem  21618  znunithash  21626  iporthcom  21696  lindfres  21886  islindf3  21889  lindsmm  21891  lmimlbs  21899  lbslcic  21904  coe1sfi  22256  coe1mul2lem2  22312  resthauslem  23412  sshauslem  23421  basqtop  23760  tgqtop  23761  hmeoopn  23815  hmeocld  23816  hmeontr  23818  hmeoimaf1o  23819  haushmphlem  23836  tsmsf1o  24194  imasdsf1olem  24424  imasf1oxmet  24426  imasf1oxms  24543  ovoliunlem1  25576  dyadmbl  25674  vitalilem3  25684  dvcnvlem  26054  dvne0f1  26091  dvcnvrelem2  26097  logf1o2  26730  dvlog  26731  wilthlem3  27151  istrkg2ld  28506  f1otrg  28917  axcontlem10  29026  usgrf1  29227  usgrexmplef  29314  usgrres1  29370  edgusgrnbfin  29428  usgrexilem  29495  sizusglecusglem1  29517  uspgr2wlkeq  29702  trlres  29756  usgr2trlncl  29816  clwlkclwwlk  30054  adjbd1o  32137  padct  32753  s1f1  32929  s2f1  32931  mndlactf1o  33036  mndractf1o  33037  cycpmconjv  33155  1arithidomlem2  33549  lmimdim  33636  madjusmdetlem4  33796  tpr2rico  33878  qqhre  33986  indf1ofs  34010  eulerpartgbij  34357  eulerpartlemgh  34363  ballotlemscr  34503  ballotlemro  34507  ballotlemfrc  34511  ballotlemrinv0  34517  reprpmtf1o  34623  derangenlem  35159  subfacp1lem3  35170  subfacp1lem5  35172  erdsze2lem1  35191  cvmliftmolem1  35269  cvmlift2lem9a  35291  phpreu  37584  poimirlem1  37601  poimirlem4  37604  poimirlem9  37609  poimirlem22  37622  mblfinlem2  37638  metf1o  37735  ismtyima  37783  ismtyres  37788  rngoisocnv  37961  laut11  40063  diaf1oN  41107  mapdcnvcl  41629  mapdcnvid2  41634  ricdrng1  42502  evlselv  42561  eldioph2lem2  42736  eldioph2  42737  pwfi2f1o  43072  gicabl  43075  sge0f1o  46321  nnfoctbdjlem  46394  3f1oss1  47008  f1ocof1ob2  47015  f1oresf1o  47223  fundcmpsurbijinjpreimafv  47315  fundcmpsurinjpreimafv  47316  fundcmpsurinjimaid  47319  isuspgrim0lem  47789  isuspgrim0  47790  uspgrimprop  47791  isuspgrimlem  47792  grimcnv  47797  uhgrimisgrgriclem  47816  uhgrimisgrgric  47817  clnbgrgrimlem  47819  grimedg  47821  grtriproplem  47824  grtrif1o  47827  grimgrtri  47832  grlimgrtri  47854  usgrexmpl1lem  47870  usgrexmpl2lem  47875  gpgusgra  47901