Theorem f1of1 6781

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

Syntax hints:   → wi 4  –1-1→wf1 6497  –onto→wfo 6498  –1-1-onto→wf1o 6499

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 6507

This theorem is referenced by:  f1of  6782  f1un  6802  f1sng  6825  f1oresrab  7082  f1ounsn  7228  f1prex  7240  f1ocnvfvrneq  7242  f1ocoima  7259  isof1oidb  7280  isores3  7291  isoini2  7295  isosolem  7303  f1oiso  7307  weniso  7310  weisoeq  7311  f1opw2  7623  f1ovv  7912  mptcnfimad  7940  tposf12  8203  oacomf1olem  8501  enssdom  8925  enssdomOLD  8926  domssex2  9077  mapen  9081  ssenen  9091  ssfiALT  9110  ssdomfi  9132  ssdomfi2  9133  sucdom2  9139  phplem2  9141  php3  9145  snnen2o  9157  1sdom2dom  9166  f1finf1o  9185  domunfican  9234  fiint  9239  f1opwfi  9268  mapfienlem1  9320  mapfienlem2  9321  mapfien  9323  marypha1lem  9348  ordtypelem10  9444  oiexg  9452  unxpwdom2  9505  wemapwe  9618  inlresf1  9839  inrresf1  9841  isinffi  9916  infxpenlem  9935  fseqenlem1  9946  dfac12lem2  10067  dfac12r  10069  ackbij2  10164  cff1  10180  infpssrlem4  10228  fin4en1  10231  enfin2i  10243  fin23lem28  10262  isf32lem7  10281  isf34lem3  10297  enfin1ai  10306  canthnum  10572  canthwe  10574  canthp1lem2  10576  pwfseqlem4  10585  pwfseqlem5  10586  tskuni  10706  grothomex  10752  negfi  12103  seqf1olem1  13976  hashfacen  14389  hashf1lem1  14390  fsumss  15660  ackbijnn  15763  fprodss  15883  bitsinv2  16382  bitsf1  16385  sadasslem  16409  sadeq  16411  phimullem  16718  eulerthlem2  16721  unbenlem  16848  f1ocpbllem  17457  f1ovscpbl  17459  xpsff1o2  17502  xpsmnd  18714  injsubmefmnd  18834  xpsgrp  19001  eqgen  19122  conjsubgen  19192  subggim  19207  gim0to0  19210  gicsubgen  19220  symgfvne  19322  symgextf1  19362  symgfixelsi  19376  f1omvdmvd  19384  f1omvdconj  19387  pmtrfconj  19407  odngen  19518  sylow1lem2  19540  sylow2blem1  19561  gsumzres  19850  gsumzcl2  19851  gsumzf1o  19853  gsumzaddlem  19862  gsumconst  19875  gsumzmhm  19878  gsumzoppg  19885  dprdf1o  19975  xpsrngd  20126  xpsringd  20280  gsumfsum  21401  zntoslem  21523  znunithash  21531  iporthcom  21602  lindfres  21790  islindf3  21793  lindsmm  21795  lmimlbs  21803  lbslcic  21808  coe1sfi  22166  coe1mul2lem2  22222  resthauslem  23319  sshauslem  23328  basqtop  23667  tgqtop  23668  hmeoopn  23722  hmeocld  23723  hmeontr  23725  hmeoimaf1o  23726  haushmphlem  23743  tsmsf1o  24101  imasdsf1olem  24329  imasf1oxmet  24331  imasf1oxms  24445  ovoliunlem1  25471  dyadmbl  25569  vitalilem3  25579  dvcnvlem  25948  dvne0f1  25985  dvcnvrelem2  25991  logf1o2  26627  dvlog  26628  wilthlem3  27048  oldfib  28385  istrkg2ld  28544  f1otrg  28955  axcontlem10  29058  usgrf1  29257  usgrexmplef  29344  usgrres1  29400  edgusgrnbfin  29458  usgrexilem  29525  sizusglecusglem1  29547  uspgr2wlkeq  29731  trlres  29784  usgr2trlncl  29845  clwlkclwwlk  30089  adjbd1o  32173  padct  32808  indf1ofs  32959  s1f1  33036  s2f1  33038  mndlactf1o  33123  mndractf1o  33124  gsumwrd2dccat  33172  cycpmconjv  33236  1arithidomlem2  33629  mplvrpmlem  33720  mplvrpmfgalem  33721  mplvrpmga  33722  mplvrpmmhm  33723  mplvrpmrhm  33724  esplysply  33748  lmimdim  33781  madjusmdetlem4  34008  tpr2rico  34090  qqhre  34198  eulerpartgbij  34550  eulerpartlemgh  34556  ballotlemscr  34697  ballotlemro  34701  ballotlemfrc  34705  ballotlemrinv0  34711  reprpmtf1o  34804  onvf1od  35323  vonf1owev  35324  derangenlem  35387  subfacp1lem3  35398  subfacp1lem5  35400  erdsze2lem1  35419  cvmliftmolem1  35497  cvmlift2lem9a  35519  phpreu  37855  poimirlem1  37872  poimirlem4  37875  poimirlem9  37880  poimirlem22  37893  mblfinlem2  37909  metf1o  38006  ismtyima  38054  ismtyres  38059  rngoisocnv  38232  laut11  40462  diaf1oN  41506  mapdcnvcl  42028  mapdcnvid2  42033  ricdrng1  42898  evlselv  42945  eldioph2lem2  43118  eldioph2  43119  pwfi2f1o  43453  gicabl  43456  permaxext  45361  permac8prim  45370  sge0f1o  46740  nnfoctbdjlem  46813  3f1oss1  47435  f1ocof1ob2  47442  f1oresf1o  47650  fundcmpsurbijinjpreimafv  47767  fundcmpsurinjpreimafv  47768  fundcmpsurinjimaid  47771  grimcnv  48248  uhgrimedg  48251  isuspgrim0lem  48253  isuspgrim0  48254  isuspgrimlem  48255  upgrimtrlslem2  48265  upgrimpthslem2  48268  uhgrimisgrgriclem  48290  uhgrimisgrgric  48291  clnbgrgrimlem  48293  grimedg  48295  grtriproplem  48299  grtrif1o  48302  grimgrtri  48309  stgrusgra  48319  isubgr3stgrlem4  48329  isubgr3stgrlem7  48332  isubgr3stgrlem8  48333  grlimgrtri  48363  usgrexmpl1lem  48381  usgrexmpl2lem  48386  gpgusgra  48417  imaidfu  49469  uptrlem1  49569