Theorem f1of1 6820

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

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

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 6544

This theorem is referenced by:  f1of  6821  f1un  6842  f1sng  6865  f1oresrab  7124  f1ounsn  7271  f1prex  7283  f1ocnvfvrneq  7285  f1ocoima  7302  isof1oidb  7323  isores3  7334  isoini2  7338  isosolem  7346  f1oiso  7350  weniso  7353  weisoeq  7354  f1opw2  7666  f1ovv  7954  mptcnfimad  7982  tposf12  8246  oacomf1olem  8548  enssdom  8972  enssdomOLD  8973  domssex2  9124  mapen  9128  ssenen  9138  ssfiALT  9157  ssdomfi  9179  ssdomfi2  9180  sucdom2  9186  phplem2  9188  php3  9192  snnen2o  9204  1sdom2dom  9213  f1finf1o  9232  domunfican  9280  fiint  9285  f1opwfi  9312  mapfienlem1  9364  mapfienlem2  9365  mapfien  9367  marypha1lem  9392  ordtypelem10  9488  oiexg  9496  unxpwdom2  9549  wemapwe  9665  inlresf1  9900  inrresf1  9902  isinffi  9977  infxpenlem  9996  fseqenlem1  10007  dfac12lem2  10127  dfac12r  10129  ackbij2  10224  cff1  10241  infpssrlem4  10289  fin4en1  10292  enfin2i  10304  fin23lem28  10323  isf32lem7  10342  isf34lem3  10358  enfin1ai  10367  canthnum  10633  canthwe  10635  canthp1lem2  10637  pwfseqlem4  10646  pwfseqlem5  10647  tskuni  10767  grothomex  10813  negfi  12163  seqf1olem1  14076  hashfacen  14490  hashf1lem1  14491  fsumss  15775  ackbijnn  15881  fprodss  16001  bitsinv2  16500  bitsf1  16503  sadasslem  16527  sadeq  16529  phimullem  16837  eulerthlem2  16840  unbenlem  16967  f1ocpbllem  17577  f1ovscpbl  17579  xpsff1o2  17622  xpsmnd  18834  injsubmefmnd  18955  xpsgrp  19124  eqgen  19248  conjsubgen  19320  subggim  19335  gim0to0  19338  gicsubgen  19348  symgfvne  19450  symgextf1  19490  symgfixelsi  19504  f1omvdmvd  19512  f1omvdconj  19515  pmtrfconj  19535  odngen  19646  sylow1lem2  19668  sylow2blem1  19689  gsumzres  19978  gsumzcl2  19979  gsumzf1o  19981  gsumzaddlem  19990  gsumconst  20003  gsumzmhm  20006  gsumzoppg  20013  dprdf1o  20103  xpsrngd  20256  xpsringd  20413  gsumfsum  21552  zntoslem  21674  znunithash  21682  iporthcom  21753  lindfres  21941  islindf3  21944  lindsmm  21946  lmimlbs  21954  lbslcic  21959  coe1sfi  22341  coe1mul2lem2  22397  resthauslem  23488  sshauslem  23497  basqtop  23836  tgqtop  23837  hmeoopn  23891  hmeocld  23892  hmeontr  23894  hmeoimaf1o  23895  haushmphlem  23912  tsmsf1o  24270  imasdsf1olem  24498  imasf1oxmet  24500  imasf1oxms  24614  ovoliunlem1  25629  dyadmbl  25727  vitalilem3  25737  dvcnvlem  26103  dvne0f1  26139  dvcnvrelem2  26145  logf1o2  26780  dvlog  26781  wilthlem3  27199  oldfib  28535  istrkg2ld  28694  f1otrg  29160  axcontlem10  29263  usgrf1  29462  usgrexmplef  29549  usgrres1  29605  edgusgrnbfin  29663  usgrexilem  29730  sizusglecusglem1  29751  uspgr2wlkeq  29935  trlres  29988  usgr2trlncl  30049  clwlkclwwlk  30293  adjbd1o  32377  padct  33003  indf1ofs  33126  s1f1  33203  s2f1  33205  mndlactf1o  33290  mndractf1o  33291  gsumwrd2dccat  33338  cycpmconjv  33402  1arithidomlem2  33770  mplvrpmlem  33877  mplvrpmfgalem  33878  mplvrpmga  33879  mplvrpmmhm  33880  mplvrpmrhm  33881  esplysply  33905  lmimdim  33938  madjusmdetlem4  34164  tpr2rico  34246  qqhre  34354  eulerpartgbij  34706  eulerpartlemgh  34712  ballotlemscr  34853  ballotlemro  34857  ballotlemfrc  34861  ballotlemrinv0  34867  reprpmtf1o  34957  onvf1od  35489  vonf1owev  35491  vonf1owevOLD  35492  vonf1oonf1  35496  derangenlem  35561  subfacp1lem3  35572  subfacp1lem5  35574  erdsze2lem1  35593  cvmliftmolem1  35671  cvmlift2lem9a  35693  phpreu  38142  poimirlem1  38159  poimirlem4  38162  poimirlem9  38167  poimirlem22  38180  mblfinlem2  38196  metf1o  38293  ismtyima  38341  ismtyres  38346  rngoisocnv  38519  laut11  40749  diaf1oN  41793  mapdcnvcl  42315  mapdcnvid2  42320  ricdrng1  43187  evlselv  43212  eldioph2lem2  43383  eldioph2  43384  pwfi2f1o  43714  gicabl  43717  permaxext  45605  permac8prim  45614  sge0f1o  46987  nnfoctbdjlem  47060  3f1oss1  47700  f1ocof1ob2  47707  f1oresf1o  47915  fundcmpsurbijinjpreimafv  48044  fundcmpsurinjpreimafv  48045  fundcmpsurinjimaid  48048  grimcnv  48541  uhgrimedg  48544  isuspgrim0lem  48546  isuspgrim0  48547  isuspgrimlem  48548  upgrimtrlslem2  48558  upgrimpthslem2  48561  uhgrimisgrgriclem  48583  uhgrimisgrgric  48584  clnbgrgrimlem  48586  grimedg  48588  grtriproplem  48592  grtrif1o  48595  grimgrtri  48602  stgrusgra  48612  isubgr3stgrlem4  48622  isubgr3stgrlem7  48625  isubgr3stgrlem8  48626  grlimgrtri  48656  usgrexmpl1lem  48674  usgrexmpl2lem  48679  gpgusgra  48710  imaidfu  49772  uptrlem1  49872