Theorem f1of1 6779

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

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

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 6505

This theorem is referenced by:  f1of  6780  f1un  6800  f1sng  6823  f1oresrab  7080  f1ounsn  7227  f1prex  7239  f1ocnvfvrneq  7241  f1ocoima  7258  isof1oidb  7279  isores3  7290  isoini2  7294  isosolem  7302  f1oiso  7306  weniso  7309  weisoeq  7310  f1opw2  7622  f1ovv  7911  mptcnfimad  7939  tposf12  8201  oacomf1olem  8499  enssdom  8923  enssdomOLD  8924  domssex2  9075  mapen  9079  ssenen  9089  ssfiALT  9108  ssdomfi  9130  ssdomfi2  9131  sucdom2  9137  phplem2  9139  php3  9143  snnen2o  9155  1sdom2dom  9164  f1finf1o  9183  domunfican  9232  fiint  9237  f1opwfi  9266  mapfienlem1  9318  mapfienlem2  9319  mapfien  9321  marypha1lem  9346  ordtypelem10  9442  oiexg  9450  unxpwdom2  9503  wemapwe  9618  inlresf1  9839  inrresf1  9841  isinffi  9916  infxpenlem  9935  fseqenlem1  9946  dfac12lem2  10067  dfac12r  10069  ackbij2  10164  cff1  10180  infpssrlem4  10228  fin4en1  10231  enfin2i  10243  fin23lem28  10262  isf32lem7  10281  isf34lem3  10297  enfin1ai  10306  canthnum  10572  canthwe  10574  canthp1lem2  10576  pwfseqlem4  10585  pwfseqlem5  10586  tskuni  10706  grothomex  10752  negfi  12105  seqf1olem1  14003  hashfacen  14416  hashf1lem1  14417  fsumss  15687  ackbijnn  15793  fprodss  15913  bitsinv2  16412  bitsf1  16415  sadasslem  16439  sadeq  16441  phimullem  16749  eulerthlem2  16752  unbenlem  16879  f1ocpbllem  17488  f1ovscpbl  17490  xpsff1o2  17533  xpsmnd  18745  injsubmefmnd  18865  xpsgrp  19035  eqgen  19156  conjsubgen  19226  subggim  19241  gim0to0  19244  gicsubgen  19254  symgfvne  19356  symgextf1  19396  symgfixelsi  19410  f1omvdmvd  19418  f1omvdconj  19421  pmtrfconj  19441  odngen  19552  sylow1lem2  19574  sylow2blem1  19595  gsumzres  19884  gsumzcl2  19885  gsumzf1o  19887  gsumzaddlem  19896  gsumconst  19909  gsumzmhm  19912  gsumzoppg  19919  dprdf1o  20009  xpsrngd  20160  xpsringd  20312  gsumfsum  21414  zntoslem  21536  znunithash  21544  iporthcom  21615  lindfres  21803  islindf3  21806  lindsmm  21808  lmimlbs  21816  lbslcic  21821  coe1sfi  22177  coe1mul2lem2  22233  resthauslem  23328  sshauslem  23337  basqtop  23676  tgqtop  23677  hmeoopn  23731  hmeocld  23732  hmeontr  23734  hmeoimaf1o  23735  haushmphlem  23752  tsmsf1o  24110  imasdsf1olem  24338  imasf1oxmet  24340  imasf1oxms  24454  ovoliunlem1  25469  dyadmbl  25567  vitalilem3  25577  dvcnvlem  25943  dvne0f1  25979  dvcnvrelem2  25985  logf1o2  26614  dvlog  26615  wilthlem3  27033  oldfib  28369  istrkg2ld  28528  f1otrg  28939  axcontlem10  29042  usgrf1  29241  usgrexmplef  29328  usgrres1  29384  edgusgrnbfin  29442  usgrexilem  29509  sizusglecusglem1  29530  uspgr2wlkeq  29714  trlres  29767  usgr2trlncl  29828  clwlkclwwlk  30072  adjbd1o  32156  padct  32791  indf1ofs  32926  s1f1  33003  s2f1  33005  mndlactf1o  33090  mndractf1o  33091  gsumwrd2dccat  33139  cycpmconjv  33203  1arithidomlem2  33596  mplvrpmlem  33687  mplvrpmfgalem  33688  mplvrpmga  33689  mplvrpmmhm  33690  mplvrpmrhm  33691  esplysply  33715  lmimdim  33748  madjusmdetlem4  33974  tpr2rico  34056  qqhre  34164  eulerpartgbij  34516  eulerpartlemgh  34522  ballotlemscr  34663  ballotlemro  34667  ballotlemfrc  34671  ballotlemrinv0  34677  reprpmtf1o  34770  onvf1od  35289  vonf1owev  35290  derangenlem  35353  subfacp1lem3  35364  subfacp1lem5  35366  erdsze2lem1  35385  cvmliftmolem1  35463  cvmlift2lem9a  35485  phpreu  37925  poimirlem1  37942  poimirlem4  37945  poimirlem9  37950  poimirlem22  37963  mblfinlem2  37979  metf1o  38076  ismtyima  38124  ismtyres  38129  rngoisocnv  38302  laut11  40532  diaf1oN  41576  mapdcnvcl  42098  mapdcnvid2  42103  ricdrng1  42973  evlselv  43020  eldioph2lem2  43193  eldioph2  43194  pwfi2f1o  43524  gicabl  43527  permaxext  45432  permac8prim  45441  sge0f1o  46810  nnfoctbdjlem  46883  3f1oss1  47523  f1ocof1ob2  47530  f1oresf1o  47738  fundcmpsurbijinjpreimafv  47867  fundcmpsurinjpreimafv  47868  fundcmpsurinjimaid  47871  grimcnv  48364  uhgrimedg  48367  isuspgrim0lem  48369  isuspgrim0  48370  isuspgrimlem  48371  upgrimtrlslem2  48381  upgrimpthslem2  48384  uhgrimisgrgriclem  48406  uhgrimisgrgric  48407  clnbgrgrimlem  48409  grimedg  48411  grtriproplem  48415  grtrif1o  48418  grimgrtri  48425  stgrusgra  48435  isubgr3stgrlem4  48445  isubgr3stgrlem7  48448  isubgr3stgrlem8  48449  grlimgrtri  48479  usgrexmpl1lem  48497  usgrexmpl2lem  48502  gpgusgra  48533  imaidfu  49585  uptrlem1  49685