Theorem f1of1 6773

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

Syntax hints:   → wi 4  –1-1→wf1 6489  –onto→wfo 6490  –1-1-onto→wf1o 6491

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 6499

This theorem is referenced by:  f1of  6774  f1un  6794  f1sng  6817  f1oresrab  7072  f1ounsn  7218  f1prex  7230  f1ocnvfvrneq  7232  f1ocoima  7249  isof1oidb  7270  isores3  7281  isoini2  7285  isosolem  7293  f1oiso  7297  weniso  7300  weisoeq  7301  f1opw2  7613  f1ovv  7902  mptcnfimad  7930  tposf12  8193  oacomf1olem  8491  enssdom  8913  enssdomOLD  8914  domssex2  9065  mapen  9069  ssenen  9079  ssfiALT  9098  ssdomfi  9120  ssdomfi2  9121  sucdom2  9127  phplem2  9129  php3  9133  snnen2o  9145  1sdom2dom  9154  f1finf1o  9173  domunfican  9222  fiint  9227  f1opwfi  9256  mapfienlem1  9308  mapfienlem2  9309  mapfien  9311  marypha1lem  9336  ordtypelem10  9432  oiexg  9440  unxpwdom2  9493  wemapwe  9606  inlresf1  9827  inrresf1  9829  isinffi  9904  infxpenlem  9923  fseqenlem1  9934  dfac12lem2  10055  dfac12r  10057  ackbij2  10152  cff1  10168  infpssrlem4  10216  fin4en1  10219  enfin2i  10231  fin23lem28  10250  isf32lem7  10269  isf34lem3  10285  enfin1ai  10294  canthnum  10560  canthwe  10562  canthp1lem2  10564  pwfseqlem4  10573  pwfseqlem5  10574  tskuni  10694  grothomex  10740  negfi  12091  seqf1olem1  13964  hashfacen  14377  hashf1lem1  14378  fsumss  15648  ackbijnn  15751  fprodss  15871  bitsinv2  16370  bitsf1  16373  sadasslem  16397  sadeq  16399  phimullem  16706  eulerthlem2  16709  unbenlem  16836  f1ocpbllem  17445  f1ovscpbl  17447  xpsff1o2  17490  xpsmnd  18702  injsubmefmnd  18822  xpsgrp  18989  eqgen  19110  conjsubgen  19180  subggim  19195  gim0to0  19198  gicsubgen  19208  symgfvne  19310  symgextf1  19350  symgfixelsi  19364  f1omvdmvd  19372  f1omvdconj  19375  pmtrfconj  19395  odngen  19506  sylow1lem2  19528  sylow2blem1  19549  gsumzres  19838  gsumzcl2  19839  gsumzf1o  19841  gsumzaddlem  19850  gsumconst  19863  gsumzmhm  19866  gsumzoppg  19873  dprdf1o  19963  xpsrngd  20114  xpsringd  20268  gsumfsum  21389  zntoslem  21511  znunithash  21519  iporthcom  21590  lindfres  21778  islindf3  21781  lindsmm  21783  lmimlbs  21791  lbslcic  21796  coe1sfi  22154  coe1mul2lem2  22210  resthauslem  23307  sshauslem  23316  basqtop  23655  tgqtop  23656  hmeoopn  23710  hmeocld  23711  hmeontr  23713  hmeoimaf1o  23714  haushmphlem  23731  tsmsf1o  24089  imasdsf1olem  24317  imasf1oxmet  24319  imasf1oxms  24433  ovoliunlem1  25459  dyadmbl  25557  vitalilem3  25567  dvcnvlem  25936  dvne0f1  25973  dvcnvrelem2  25979  logf1o2  26615  dvlog  26616  wilthlem3  27036  oldfib  28373  istrkg2ld  28532  f1otrg  28943  axcontlem10  29046  usgrf1  29245  usgrexmplef  29332  usgrres1  29388  edgusgrnbfin  29446  usgrexilem  29513  sizusglecusglem1  29535  uspgr2wlkeq  29719  trlres  29772  usgr2trlncl  29833  clwlkclwwlk  30077  adjbd1o  32160  padct  32797  indf1ofs  32948  s1f1  33025  s2f1  33027  mndlactf1o  33112  mndractf1o  33113  gsumwrd2dccat  33160  cycpmconjv  33224  1arithidomlem2  33617  mplvrpmlem  33708  mplvrpmfgalem  33709  mplvrpmga  33710  mplvrpmmhm  33711  mplvrpmrhm  33712  esplysply  33729  lmimdim  33760  madjusmdetlem4  33987  tpr2rico  34069  qqhre  34177  eulerpartgbij  34529  eulerpartlemgh  34535  ballotlemscr  34676  ballotlemro  34680  ballotlemfrc  34684  ballotlemrinv0  34690  reprpmtf1o  34783  onvf1od  35301  vonf1owev  35302  derangenlem  35365  subfacp1lem3  35376  subfacp1lem5  35378  erdsze2lem1  35397  cvmliftmolem1  35475  cvmlift2lem9a  35497  phpreu  37805  poimirlem1  37822  poimirlem4  37825  poimirlem9  37830  poimirlem22  37843  mblfinlem2  37859  metf1o  37956  ismtyima  38004  ismtyres  38009  rngoisocnv  38182  laut11  40346  diaf1oN  41390  mapdcnvcl  41912  mapdcnvid2  41917  ricdrng1  42783  evlselv  42830  eldioph2lem2  43003  eldioph2  43004  pwfi2f1o  43338  gicabl  43341  permaxext  45246  permac8prim  45255  sge0f1o  46626  nnfoctbdjlem  46699  3f1oss1  47321  f1ocof1ob2  47328  f1oresf1o  47536  fundcmpsurbijinjpreimafv  47653  fundcmpsurinjpreimafv  47654  fundcmpsurinjimaid  47657  grimcnv  48134  uhgrimedg  48137  isuspgrim0lem  48139  isuspgrim0  48140  isuspgrimlem  48141  upgrimtrlslem2  48151  upgrimpthslem2  48154  uhgrimisgrgriclem  48176  uhgrimisgrgric  48177  clnbgrgrimlem  48179  grimedg  48181  grtriproplem  48185  grtrif1o  48188  grimgrtri  48195  stgrusgra  48205  isubgr3stgrlem4  48215  isubgr3stgrlem7  48218  isubgr3stgrlem8  48219  grlimgrtri  48249  usgrexmpl1lem  48267  usgrexmpl2lem  48272  gpgusgra  48303  imaidfu  49355  uptrlem1  49455