Theorem f1of1 6861

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

Syntax hints:   → wi 4  –1-1→wf1 6570  –onto→wfo 6571  –1-1-onto→wf1o 6572

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 6580

This theorem is referenced by:  f1of  6862  f1un  6882  f1sng  6904  f1oresrab  7161  f1prex  7320  f1ocnvfvrneq  7322  f1ocoima  7339  isof1oidb  7360  isores3  7371  isoini2  7375  isosolem  7383  f1oiso  7387  weniso  7390  weisoeq  7391  f1opw2  7705  f1ovv  7998  mptcnfimad  8027  tposf12  8292  oacomf1olem  8620  enssdom  9037  sucdom2OLD  9148  domssex2  9203  mapen  9207  ssenen  9217  ssfiALT  9241  ssdomfi  9262  ssdomfi2  9263  sucdom2  9269  phplem2  9271  php3  9275  phplem4OLD  9283  php3OLD  9287  snnen2o  9300  1sdom2dom  9310  f1finf1o  9333  f1finf1oOLD  9334  domunfican  9389  fiint  9394  fiintOLD  9395  f1opwfi  9426  mapfienlem1  9474  mapfienlem2  9475  mapfien  9477  marypha1lem  9502  ordtypelem10  9596  oiexg  9604  unxpwdom2  9657  wemapwe  9766  inlresf1  9984  inrresf1  9986  isinffi  10061  infxpenlem  10082  fseqenlem1  10093  dfac12lem2  10214  dfac12r  10216  ackbij2  10311  cff1  10327  infpssrlem4  10375  fin4en1  10378  enfin2i  10390  fin23lem28  10409  isf32lem7  10428  isf34lem3  10444  enfin1ai  10453  canthnum  10718  canthwe  10720  canthp1lem2  10722  pwfseqlem4  10731  pwfseqlem5  10732  tskuni  10852  grothomex  10898  negfi  12244  seqf1olem1  14092  hashfacen  14503  hashf1lem1  14504  fsumss  15773  ackbijnn  15876  fprodss  15996  bitsinv2  16489  bitsf1  16492  sadasslem  16516  sadeq  16518  phimullem  16826  eulerthlem2  16829  unbenlem  16955  f1ocpbllem  17584  f1ovscpbl  17586  xpsff1o2  17629  xpsmnd  18812  injsubmefmnd  18932  xpsgrp  19099  eqgen  19221  conjsubgen  19291  subggim  19306  gim0to0  19309  gicsubgen  19319  symgfvne  19422  symgextf1  19463  symgfixelsi  19477  f1omvdmvd  19485  f1omvdconj  19488  pmtrfconj  19508  odngen  19619  sylow1lem2  19641  sylow2blem1  19662  gsumzres  19951  gsumzcl2  19952  gsumzf1o  19954  gsumzaddlem  19963  gsumconst  19976  gsumzmhm  19979  gsumzoppg  19986  dprdf1o  20076  xpsrngd  20206  xpsringd  20355  gsumfsum  21475  zntoslem  21598  znunithash  21606  iporthcom  21676  lindfres  21866  islindf3  21869  lindsmm  21871  lmimlbs  21879  lbslcic  21884  coe1sfi  22236  coe1mul2lem2  22292  resthauslem  23392  sshauslem  23401  basqtop  23740  tgqtop  23741  hmeoopn  23795  hmeocld  23796  hmeontr  23798  hmeoimaf1o  23799  haushmphlem  23816  tsmsf1o  24174  imasdsf1olem  24404  imasf1oxmet  24406  imasf1oxms  24523  ovoliunlem1  25556  dyadmbl  25654  vitalilem3  25664  dvcnvlem  26034  dvne0f1  26071  dvcnvrelem2  26077  logf1o2  26710  dvlog  26711  wilthlem3  27131  istrkg2ld  28486  f1otrg  28897  axcontlem10  29006  usgrf1  29207  usgrexmplef  29294  usgrres1  29350  edgusgrnbfin  29408  usgrexilem  29475  sizusglecusglem1  29497  uspgr2wlkeq  29682  trlres  29736  usgr2trlncl  29796  clwlkclwwlk  30034  adjbd1o  32117  padct  32733  s1f1  32909  s2f1  32911  mndlactf1o  33016  mndractf1o  33017  cycpmconjv  33135  1arithidomlem2  33529  lmimdim  33616  madjusmdetlem4  33776  tpr2rico  33858  qqhre  33966  indf1ofs  33990  eulerpartgbij  34337  eulerpartlemgh  34343  ballotlemscr  34483  ballotlemro  34487  ballotlemfrc  34491  ballotlemrinv0  34497  reprpmtf1o  34603  derangenlem  35139  subfacp1lem3  35150  subfacp1lem5  35152  erdsze2lem1  35171  cvmliftmolem1  35249  cvmlift2lem9a  35271  phpreu  37564  poimirlem1  37581  poimirlem4  37584  poimirlem9  37589  poimirlem22  37602  mblfinlem2  37618  metf1o  37715  ismtyima  37763  ismtyres  37768  rngoisocnv  37941  laut11  40043  diaf1oN  41087  mapdcnvcl  41609  mapdcnvid2  41614  ricdrng1  42483  evlselv  42542  eldioph2lem2  42717  eldioph2  42718  pwfi2f1o  43053  gicabl  43056  sge0f1o  46303  nnfoctbdjlem  46376  3f1oss1  46990  f1ocof1ob2  46997  f1oresf1o  47205  fundcmpsurbijinjpreimafv  47281  fundcmpsurinjpreimafv  47282  fundcmpsurinjimaid  47285  isuspgrim0lem  47755  isuspgrim0  47756  uspgrimprop  47757  isuspgrimlem  47758  grimcnv  47763  uhgrimisgrgriclem  47782  uhgrimisgrgric  47783  clnbgrgrimlem  47785  grimedg  47787  grtriproplem  47790  grtrif1o  47793  grimgrtri  47798  grlimgrtri  47820  usgrexmpl1lem  47836  usgrexmpl2lem  47841