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  7955  mptcnfimad  7983  tposf12  8247  oacomf1olem  8549  enssdom  8973  enssdomOLD  8974  domssex2  9125  mapen  9129  ssenen  9139  ssfiALT  9158  ssdomfi  9180  ssdomfi2  9181  sucdom2  9187  phplem2  9189  php3  9193  snnen2o  9205  1sdom2dom  9214  f1finf1o  9233  domunfican  9281  fiint  9286  f1opwfi  9313  mapfienlem1  9365  mapfienlem2  9366  mapfien  9368  marypha1lem  9393  ordtypelem10  9489  oiexg  9497  unxpwdom2  9550  wemapwe  9666  inlresf1  9901  inrresf1  9903  isinffi  9978  infxpenlem  9997  fseqenlem1  10008  dfac12lem2  10128  dfac12r  10130  ackbij2  10225  cff1  10242  infpssrlem4  10290  fin4en1  10293  enfin2i  10305  fin23lem28  10324  isf32lem7  10343  isf34lem3  10359  enfin1ai  10368  canthnum  10634  canthwe  10636  canthp1lem2  10638  pwfseqlem4  10647  pwfseqlem5  10648  tskuni  10768  grothomex  10814  negfi  12164  seqf1olem1  14077  hashfacen  14491  hashf1lem1  14492  fsumss  15776  ackbijnn  15882  fprodss  16002  bitsinv2  16501  bitsf1  16504  sadasslem  16528  sadeq  16530  phimullem  16838  eulerthlem2  16841  unbenlem  16968  f1ocpbllem  17578  f1ovscpbl  17580  xpsff1o2  17623  xpsmnd  18835  injsubmefmnd  18956  xpsgrp  19125  eqgen  19249  conjsubgen  19321  subggim  19336  gim0to0  19339  gicsubgen  19349  symgfvne  19451  symgextf1  19491  symgfixelsi  19505  f1omvdmvd  19513  f1omvdconj  19516  pmtrfconj  19536  odngen  19647  sylow1lem2  19669  sylow2blem1  19690  gsumzres  19979  gsumzcl2  19980  gsumzf1o  19982  gsumzaddlem  19991  gsumconst  20004  gsumzmhm  20007  gsumzoppg  20014  dprdf1o  20104  xpsrngd  20257  xpsringd  20414  gsumfsum  21553  zntoslem  21675  znunithash  21683  iporthcom  21754  lindfres  21942  islindf3  21945  lindsmm  21947  lmimlbs  21955  lbslcic  21960  coe1sfi  22342  coe1mul2lem2  22398  resthauslem  23489  sshauslem  23498  basqtop  23837  tgqtop  23838  hmeoopn  23892  hmeocld  23893  hmeontr  23895  hmeoimaf1o  23896  haushmphlem  23913  tsmsf1o  24271  imasdsf1olem  24499  imasf1oxmet  24501  imasf1oxms  24615  ovoliunlem1  25630  dyadmbl  25728  vitalilem3  25738  dvcnvlem  26104  dvne0f1  26140  dvcnvrelem2  26146  logf1o2  26781  dvlog  26782  wilthlem3  27200  oldfib  28536  istrkg2ld  28695  f1otrg  29161  axcontlem10  29264  usgrf1  29463  usgrexmplef  29550  usgrres1  29606  edgusgrnbfin  29664  usgrexilem  29731  sizusglecusglem1  29752  uspgr2wlkeq  29936  trlres  29989  usgr2trlncl  30050  clwlkclwwlk  30294  adjbd1o  32378  padct  33004  indf1ofs  33127  s1f1  33204  s2f1  33206  mndlactf1o  33291  mndractf1o  33292  gsumwrd2dccat  33339  cycpmconjv  33403  1arithidomlem2  33771  mplvrpmlem  33878  mplvrpmfgalem  33879  mplvrpmga  33880  mplvrpmmhm  33881  mplvrpmrhm  33882  esplysply  33906  lmimdim  33939  madjusmdetlem4  34165  tpr2rico  34247  qqhre  34355  eulerpartgbij  34707  eulerpartlemgh  34713  ballotlemscr  34854  ballotlemro  34858  ballotlemfrc  34862  ballotlemrinv0  34868  reprpmtf1o  34958  onvf1od  35490  vonf1owev  35492  vonf1owevOLD  35493  vonf1oonf1  35497  derangenlem  35562  subfacp1lem3  35573  subfacp1lem5  35575  erdsze2lem1  35594  cvmliftmolem1  35672  cvmlift2lem9a  35694  phpreu  38143  poimirlem1  38160  poimirlem4  38163  poimirlem9  38168  poimirlem22  38181  mblfinlem2  38197  metf1o  38294  ismtyima  38342  ismtyres  38347  rngoisocnv  38520  laut11  40750  diaf1oN  41794  mapdcnvcl  42316  mapdcnvid2  42321  ricdrng1  43188  evlselv  43213  eldioph2lem2  43384  eldioph2  43385  pwfi2f1o  43715  gicabl  43718  permaxext  45606  permac8prim  45615  sge0f1o  46988  nnfoctbdjlem  47061  3f1oss1  47701  f1ocof1ob2  47708  f1oresf1o  47916  fundcmpsurbijinjpreimafv  48045  fundcmpsurinjpreimafv  48046  fundcmpsurinjimaid  48049  grimcnv  48542  uhgrimedg  48545  isuspgrim0lem  48547  isuspgrim0  48548  isuspgrimlem  48549  upgrimtrlslem2  48559  upgrimpthslem2  48562  uhgrimisgrgriclem  48584  uhgrimisgrgric  48585  clnbgrgrimlem  48587  grimedg  48589  grtriproplem  48593  grtrif1o  48596  grimgrtri  48603  stgrusgra  48613  isubgr3stgrlem4  48623  isubgr3stgrlem7  48626  isubgr3stgrlem8  48627  grlimgrtri  48657  usgrexmpl1lem  48675  usgrexmpl2lem  48680  gpgusgra  48711  imaidfu  49773  uptrlem1  49873