Theorem f1of1 6827

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

Syntax hints:   → wi 4  –1-1→wf1 6538  –onto→wfo 6539  –1-1-onto→wf1o 6540

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 6548

This theorem is referenced by:  f1of  6828  f1un  6848  f1sng  6870  f1oresrab  7127  f1ounsn  7274  f1prex  7286  f1ocnvfvrneq  7288  f1ocoima  7305  isof1oidb  7326  isores3  7337  isoini2  7341  isosolem  7349  f1oiso  7353  weniso  7356  weisoeq  7357  f1opw2  7670  f1ovv  7964  mptcnfimad  7993  tposf12  8258  oacomf1olem  8584  enssdom  8999  sucdom2OLD  9104  domssex2  9159  mapen  9163  ssenen  9173  ssfiALT  9196  ssdomfi  9218  ssdomfi2  9219  sucdom2  9225  phplem2  9227  php3  9231  phplem4OLD  9239  php3OLD  9243  snnen2o  9255  1sdom2dom  9265  f1finf1o  9287  f1finf1oOLD  9288  domunfican  9343  fiint  9348  fiintOLD  9349  f1opwfi  9378  mapfienlem1  9427  mapfienlem2  9428  mapfien  9430  marypha1lem  9455  ordtypelem10  9549  oiexg  9557  unxpwdom2  9610  wemapwe  9719  inlresf1  9937  inrresf1  9939  isinffi  10014  infxpenlem  10035  fseqenlem1  10046  dfac12lem2  10167  dfac12r  10169  ackbij2  10264  cff1  10280  infpssrlem4  10328  fin4en1  10331  enfin2i  10343  fin23lem28  10362  isf32lem7  10381  isf34lem3  10397  enfin1ai  10406  canthnum  10671  canthwe  10673  canthp1lem2  10675  pwfseqlem4  10684  pwfseqlem5  10685  tskuni  10805  grothomex  10851  negfi  12199  seqf1olem1  14064  hashfacen  14476  hashf1lem1  14477  fsumss  15744  ackbijnn  15847  fprodss  15967  bitsinv2  16463  bitsf1  16466  sadasslem  16490  sadeq  16492  phimullem  16799  eulerthlem2  16802  unbenlem  16929  f1ocpbllem  17541  f1ovscpbl  17543  xpsff1o2  17586  xpsmnd  18760  injsubmefmnd  18880  xpsgrp  19047  eqgen  19169  conjsubgen  19239  subggim  19254  gim0to0  19257  gicsubgen  19267  symgfvne  19367  symgextf1  19408  symgfixelsi  19422  f1omvdmvd  19430  f1omvdconj  19433  pmtrfconj  19453  odngen  19564  sylow1lem2  19586  sylow2blem1  19607  gsumzres  19896  gsumzcl2  19897  gsumzf1o  19899  gsumzaddlem  19908  gsumconst  19921  gsumzmhm  19924  gsumzoppg  19931  dprdf1o  20021  xpsrngd  20145  xpsringd  20298  gsumfsum  21415  zntoslem  21530  znunithash  21538  iporthcom  21608  lindfres  21798  islindf3  21801  lindsmm  21803  lmimlbs  21811  lbslcic  21816  coe1sfi  22164  coe1mul2lem2  22220  resthauslem  23318  sshauslem  23327  basqtop  23666  tgqtop  23667  hmeoopn  23721  hmeocld  23722  hmeontr  23724  hmeoimaf1o  23725  haushmphlem  23742  tsmsf1o  24100  imasdsf1olem  24329  imasf1oxmet  24331  imasf1oxms  24447  ovoliunlem1  25474  dyadmbl  25572  vitalilem3  25582  dvcnvlem  25951  dvne0f1  25988  dvcnvrelem2  25994  logf1o2  26629  dvlog  26630  wilthlem3  27050  istrkg2ld  28405  f1otrg  28816  axcontlem10  28919  usgrf1  29118  usgrexmplef  29205  usgrres1  29261  edgusgrnbfin  29319  usgrexilem  29386  sizusglecusglem1  29408  uspgr2wlkeq  29593  trlres  29647  usgr2trlncl  29709  clwlkclwwlk  29950  adjbd1o  32033  padct  32667  indf1ofs  32796  s1f1  32872  s2f1  32874  mndlactf1o  32979  mndractf1o  32980  gsumwrd2dccat  33014  cycpmconjv  33106  1arithidomlem2  33504  lmimdim  33594  madjusmdetlem4  33804  tpr2rico  33886  qqhre  33996  eulerpartgbij  34349  eulerpartlemgh  34355  ballotlemscr  34496  ballotlemro  34500  ballotlemfrc  34504  ballotlemrinv0  34510  reprpmtf1o  34616  derangenlem  35151  subfacp1lem3  35162  subfacp1lem5  35164  erdsze2lem1  35183  cvmliftmolem1  35261  cvmlift2lem9a  35283  phpreu  37586  poimirlem1  37603  poimirlem4  37606  poimirlem9  37611  poimirlem22  37624  mblfinlem2  37640  metf1o  37737  ismtyima  37785  ismtyres  37790  rngoisocnv  37963  laut11  40063  diaf1oN  41107  mapdcnvcl  41629  mapdcnvid2  41634  ricdrng1  42517  evlselv  42576  eldioph2lem2  42750  eldioph2  42751  pwfi2f1o  43086  gicabl  43089  sge0f1o  46369  nnfoctbdjlem  46442  3f1oss1  47060  f1ocof1ob2  47067  f1oresf1o  47275  fundcmpsurbijinjpreimafv  47367  fundcmpsurinjpreimafv  47368  fundcmpsurinjimaid  47371  isuspgrim0lem  47844  isuspgrim0  47845  uspgrimprop  47846  isuspgrimlem  47847  grimcnv  47852  uhgrimisgrgriclem  47871  uhgrimisgrgric  47872  clnbgrgrimlem  47874  grimedg  47876  grtriproplem  47879  grtrif1o  47882  grimgrtri  47889  stgrusgra  47899  isubgr3stgrlem4  47909  isubgr3stgrlem7  47912  isubgr3stgrlem8  47913  grlimgrtri  47936  usgrexmpl1lem  47953  usgrexmpl2lem  47958  gpgusgra  47985