Theorem f1of1 6799

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

Syntax hints:   → wi 4  –1-1→wf1 6508  –onto→wfo 6509  –1-1-onto→wf1o 6510

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 6518

This theorem is referenced by:  f1of  6800  f1un  6820  f1sng  6842  f1oresrab  7099  f1ounsn  7247  f1prex  7259  f1ocnvfvrneq  7261  f1ocoima  7278  isof1oidb  7299  isores3  7310  isoini2  7314  isosolem  7322  f1oiso  7326  weniso  7329  weisoeq  7330  f1opw2  7644  f1ovv  7936  mptcnfimad  7965  tposf12  8230  oacomf1olem  8528  enssdom  8948  domssex2  9101  mapen  9105  ssenen  9115  ssfiALT  9138  ssdomfi  9160  ssdomfi2  9161  sucdom2  9167  phplem2  9169  php3  9173  snnen2o  9184  1sdom2dom  9194  f1finf1o  9216  f1finf1oOLD  9217  domunfican  9272  fiint  9277  fiintOLD  9278  f1opwfi  9307  mapfienlem1  9356  mapfienlem2  9357  mapfien  9359  marypha1lem  9384  ordtypelem10  9480  oiexg  9488  unxpwdom2  9541  wemapwe  9650  inlresf1  9868  inrresf1  9870  isinffi  9945  infxpenlem  9966  fseqenlem1  9977  dfac12lem2  10098  dfac12r  10100  ackbij2  10195  cff1  10211  infpssrlem4  10259  fin4en1  10262  enfin2i  10274  fin23lem28  10293  isf32lem7  10312  isf34lem3  10328  enfin1ai  10337  canthnum  10602  canthwe  10604  canthp1lem2  10606  pwfseqlem4  10615  pwfseqlem5  10616  tskuni  10736  grothomex  10782  negfi  12132  seqf1olem1  14006  hashfacen  14419  hashf1lem1  14420  fsumss  15691  ackbijnn  15794  fprodss  15914  bitsinv2  16413  bitsf1  16416  sadasslem  16440  sadeq  16442  phimullem  16749  eulerthlem2  16752  unbenlem  16879  f1ocpbllem  17487  f1ovscpbl  17489  xpsff1o2  17532  xpsmnd  18704  injsubmefmnd  18824  xpsgrp  18991  eqgen  19113  conjsubgen  19183  subggim  19198  gim0to0  19201  gicsubgen  19211  symgfvne  19311  symgextf1  19351  symgfixelsi  19365  f1omvdmvd  19373  f1omvdconj  19376  pmtrfconj  19396  odngen  19507  sylow1lem2  19529  sylow2blem1  19550  gsumzres  19839  gsumzcl2  19840  gsumzf1o  19842  gsumzaddlem  19851  gsumconst  19864  gsumzmhm  19867  gsumzoppg  19874  dprdf1o  19964  xpsrngd  20088  xpsringd  20241  gsumfsum  21351  zntoslem  21466  znunithash  21474  iporthcom  21544  lindfres  21732  islindf3  21735  lindsmm  21737  lmimlbs  21745  lbslcic  21750  coe1sfi  22098  coe1mul2lem2  22154  resthauslem  23250  sshauslem  23259  basqtop  23598  tgqtop  23599  hmeoopn  23653  hmeocld  23654  hmeontr  23656  hmeoimaf1o  23657  haushmphlem  23674  tsmsf1o  24032  imasdsf1olem  24261  imasf1oxmet  24263  imasf1oxms  24377  ovoliunlem1  25403  dyadmbl  25501  vitalilem3  25511  dvcnvlem  25880  dvne0f1  25917  dvcnvrelem2  25923  logf1o2  26559  dvlog  26560  wilthlem3  26980  istrkg2ld  28387  f1otrg  28798  axcontlem10  28900  usgrf1  29099  usgrexmplef  29186  usgrres1  29242  edgusgrnbfin  29300  usgrexilem  29367  sizusglecusglem1  29389  uspgr2wlkeq  29574  trlres  29628  usgr2trlncl  29690  clwlkclwwlk  29931  adjbd1o  32014  padct  32643  indf1ofs  32789  s1f1  32864  s2f1  32866  mndlactf1o  32971  mndractf1o  32972  gsumwrd2dccat  33007  cycpmconjv  33099  1arithidomlem2  33507  lmimdim  33599  madjusmdetlem4  33820  tpr2rico  33902  qqhre  34010  eulerpartgbij  34363  eulerpartlemgh  34369  ballotlemscr  34510  ballotlemro  34514  ballotlemfrc  34518  ballotlemrinv0  34524  reprpmtf1o  34617  onvf1od  35094  vonf1owev  35095  derangenlem  35158  subfacp1lem3  35169  subfacp1lem5  35171  erdsze2lem1  35190  cvmliftmolem1  35268  cvmlift2lem9a  35290  phpreu  37598  poimirlem1  37615  poimirlem4  37618  poimirlem9  37623  poimirlem22  37636  mblfinlem2  37652  metf1o  37749  ismtyima  37797  ismtyres  37802  rngoisocnv  37975  laut11  40080  diaf1oN  41124  mapdcnvcl  41646  mapdcnvid2  41651  ricdrng1  42516  evlselv  42575  eldioph2lem2  42749  eldioph2  42750  pwfi2f1o  43085  gicabl  43088  permaxext  44995  permac8prim  45004  sge0f1o  46380  nnfoctbdjlem  46453  3f1oss1  47076  f1ocof1ob2  47083  f1oresf1o  47291  fundcmpsurbijinjpreimafv  47408  fundcmpsurinjpreimafv  47409  fundcmpsurinjimaid  47412  grimcnv  47888  uhgrimedg  47891  isuspgrim0lem  47893  isuspgrim0  47894  isuspgrimlem  47895  upgrimtrlslem2  47905  upgrimpthslem2  47908  uhgrimisgrgriclem  47930  uhgrimisgrgric  47931  clnbgrgrimlem  47933  grimedg  47935  grtriproplem  47938  grtrif1o  47941  grimgrtri  47948  stgrusgra  47958  isubgr3stgrlem4  47968  isubgr3stgrlem7  47971  isubgr3stgrlem8  47972  grlimgrtri  47995  usgrexmpl1lem  48012  usgrexmpl2lem  48017  gpgusgra  48048  imaidfu  49099  uptrlem1  49199