Theorem f1of1 6819

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

Syntax hints:   → wi 4  –1-1→wf1 6533  –onto→wfo 6534  –1-1-onto→wf1o 6535

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 210  df-an 401  df-f1o 6543

This theorem is referenced by:  f1of  6820  f1un  6841  f1sng  6864  f1oresrab  7123  f1ounsn  7270  f1prex  7282  f1ocnvfvrneq  7284  f1ocoima  7301  isof1oidb  7322  isores3  7333  isoini2  7337  isosolem  7345  f1oiso  7349  weniso  7352  weisoeq  7353  f1opw2  7665  f1ovv  7951  mptcnfimad  7979  tposf12  8243  oacomf1olem  8545  enssdom  8969  enssdomOLD  8970  domssex2  9121  mapen  9125  ssenen  9135  ssfiALT  9154  ssdomfi  9176  ssdomfi2  9177  sucdom2  9183  phplem2  9185  php3  9189  snnen2o  9201  1sdom2dom  9210  f1finf1o  9229  domunfican  9277  fiint  9282  f1opwfi  9309  mapfienlem1  9361  mapfienlem2  9362  mapfien  9364  marypha1lem  9389  ordtypelem10  9485  oiexg  9493  unxpwdom2  9546  wemapwe  9662  inlresf1  9897  inrresf1  9899  isinffi  9974  infxpenlem  9993  fseqenlem1  10004  dfac12lem2  10124  dfac12r  10126  ackbij2  10221  cff1  10237  infpssrlem4  10285  fin4en1  10288  enfin2i  10300  fin23lem28  10319  isf32lem7  10338  isf34lem3  10354  enfin1ai  10363  canthnum  10629  canthwe  10631  canthp1lem2  10633  pwfseqlem4  10642  pwfseqlem5  10643  tskuni  10763  grothomex  10809  negfi  12159  seqf1olem1  14073  hashfacen  14487  hashf1lem1  14488  fsumss  15772  ackbijnn  15878  fprodss  15998  bitsinv2  16496  bitsf1  16499  sadasslem  16523  sadeq  16525  phimullem  16833  eulerthlem2  16836  unbenlem  16963  f1ocpbllem  17573  f1ovscpbl  17575  xpsff1o2  17618  xpsmnd  18830  injsubmefmnd  18951  xpsgrp  19120  eqgen  19244  conjsubgen  19316  subggim  19331  gim0to0  19334  gicsubgen  19344  symgfvne  19446  symgextf1  19486  symgfixelsi  19500  f1omvdmvd  19508  f1omvdconj  19511  pmtrfconj  19531  odngen  19642  sylow1lem2  19664  sylow2blem1  19685  gsumzres  19974  gsumzcl2  19975  gsumzf1o  19977  gsumzaddlem  19986  gsumconst  19999  gsumzmhm  20002  gsumzoppg  20009  dprdf1o  20099  xpsrngd  20252  xpsringd  20410  gsumfsum  21584  zntoslem  21706  znunithash  21714  iporthcom  21785  lindfres  21973  islindf3  21976  lindsmm  21978  lmimlbs  21986  lbslcic  21991  coe1sfi  22373  coe1mul2lem2  22429  resthauslem  23520  sshauslem  23529  basqtop  23868  tgqtop  23869  hmeoopn  23923  hmeocld  23924  hmeontr  23926  hmeoimaf1o  23927  haushmphlem  23944  tsmsf1o  24302  imasdsf1olem  24530  imasf1oxmet  24532  imasf1oxms  24646  ovoliunlem1  25661  dyadmbl  25759  vitalilem3  25769  dvcnvlem  26135  dvne0f1  26171  dvcnvrelem2  26177  logf1o2  26815  dvlog  26816  wilthlem3  27234  oldfib  28570  istrkg2ld  28729  f1otrg  29220  axcontlem10  29323  usgrf1  29522  usgrexmplef  29609  usgrres1  29665  edgusgrnbfin  29723  usgrexilem  29790  sizusglecusglem1  29811  uspgr2wlkeq  29995  trlres  30048  usgr2trlncl  30109  clwlkclwwlk  30353  adjbd1o  32437  padct  33063  indf1ofs  33186  s1f1  33263  s2f1  33265  mndlactf1o  33350  mndractf1o  33351  gsumwrd2dccat  33398  cycpmconjv  33462  1arithidomlem2  33826  mplvrpmlem  33933  mplvrpmfgalem  33934  mplvrpmga  33935  mplvrpmmhm  33936  mplvrpmrhm  33937  esplysply  33961  lmimdim  33994  madjusmdetlem4  34220  tpr2rico  34302  qqhre  34410  eulerpartgbij  34762  eulerpartlemgh  34768  ballotlemscr  34909  ballotlemro  34913  ballotlemfrc  34917  ballotlemrinv0  34923  reprpmtf1o  35013  onvf1od  35591  vonf1owev  35593  vonf1owevOLD  35594  vonf1oonf1  35598  derangenlem  35663  subfacp1lem3  35674  subfacp1lem5  35676  erdsze2lem1  35695  cvmliftmolem1  35773  cvmlift2lem9a  35795  phpreu  38255  poimirlem1  38272  poimirlem4  38275  poimirlem9  38280  poimirlem22  38293  mblfinlem2  38309  metf1o  38406  ismtyima  38454  ismtyres  38459  rngoisocnv  38632  laut11  40860  diaf1oN  41904  mapdcnvcl  42426  mapdcnvid2  42431  ricdrng1  43296  evlselv  43321  eldioph2lem2  43492  eldioph2  43493  pwfi2f1o  43823  gicabl  43826  permaxext  45714  permac8prim  45723  sge0f1o  47096  nnfoctbdjlem  47169  3f1oss1  47812  f1ocof1ob2  47819  f1oresf1o  48027  fundcmpsurbijinjpreimafv  48156  fundcmpsurinjpreimafv  48157  fundcmpsurinjimaid  48160  grimcnv  48653  uhgrimedg  48656  isuspgrim0lem  48658  isuspgrim0  48659  isuspgrimlem  48660  upgrimtrlslem2  48670  upgrimpthslem2  48673  uhgrimisgrgriclem  48695  uhgrimisgrgric  48696  clnbgrgrimlem  48698  grimedg  48700  grtriproplem  48704  grtrif1o  48707  grimgrtri  48714  stgrusgra  48724  isubgr3stgrlem4  48734  isubgr3stgrlem7  48737  isubgr3stgrlem8  48738  grlimgrtri  48768  usgrexmpl1lem  48786  usgrexmpl2lem  48791  gpgusgra  48822  imaidfu  49888  uptrlem1  49988