Theorem f1of1 6833

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

Syntax hints:   → wi 4  –1-1→wf1 6541  –onto→wfo 6542  –1-1-onto→wf1o 6543

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 206  df-an 398  df-f1o 6551

This theorem is referenced by:  f1of  6834  f1un  6854  f1sng  6876  f1oresrab  7125  f1prex  7282  f1ocnvfvrneq  7284  isof1oidb  7321  isores3  7332  isoini2  7336  isosolem  7344  f1oiso  7348  weniso  7351  weisoeq  7352  f1opw2  7661  f1ovv  7944  tposf12  8236  oacomf1olem  8564  enssdom  8973  sucdom2OLD  9082  domssex2  9137  mapen  9141  ssenen  9151  ssfiALT  9174  ssdomfi  9199  ssdomfi2  9200  sucdom2  9206  phplem2  9208  php3  9212  phplem4OLD  9220  php3OLD  9224  snnen2o  9237  1sdom2dom  9247  f1finf1o  9271  f1finf1oOLD  9272  domunfican  9320  fiint  9324  f1opwfi  9356  mapfienlem1  9400  mapfienlem2  9401  mapfien  9403  marypha1lem  9428  ordtypelem10  9522  oiexg  9530  unxpwdom2  9583  wemapwe  9692  inlresf1  9910  inrresf1  9912  isinffi  9987  infxpenlem  10008  fseqenlem1  10019  dfac12lem2  10139  dfac12r  10141  ackbij2  10238  cff1  10253  infpssrlem4  10301  fin4en1  10304  enfin2i  10316  fin23lem28  10335  isf32lem7  10354  isf34lem3  10370  enfin1ai  10379  canthnum  10644  canthwe  10646  canthp1lem2  10648  pwfseqlem4  10657  pwfseqlem5  10658  tskuni  10778  grothomex  10824  negfi  12163  seqf1olem1  14007  hashfacen  14413  hashfacenOLD  14414  hashf1lem1  14415  hashf1lem1OLD  14416  fsumss  15671  ackbijnn  15774  fprodss  15892  bitsinv2  16384  bitsf1  16387  sadasslem  16411  sadeq  16413  phimullem  16712  eulerthlem2  16715  unbenlem  16841  f1ocpbllem  17470  f1ovscpbl  17472  xpsff1o2  17515  xpsmnd  18665  injsubmefmnd  18778  xpsgrp  18942  eqgen  19061  conjsubgen  19125  subggim  19140  gicsubgen  19152  symgfvne  19248  symgextf1  19289  symgfixelsi  19303  f1omvdmvd  19311  f1omvdconj  19314  pmtrfconj  19334  odngen  19445  sylow1lem2  19467  sylow2blem1  19488  gsumzres  19777  gsumzcl2  19778  gsumzf1o  19780  gsumzaddlem  19789  gsumconst  19802  gsumzmhm  19805  gsumzoppg  19812  dprdf1o  19902  xpsringd  20145  gim0to0  20281  gsumfsum  21012  zntoslem  21112  znunithash  21120  iporthcom  21188  lindfres  21378  islindf3  21381  lindsmm  21383  lmimlbs  21391  lbslcic  21396  coe1sfi  21737  coe1mul2lem2  21790  resthauslem  22867  sshauslem  22876  basqtop  23215  tgqtop  23216  hmeoopn  23270  hmeocld  23271  hmeontr  23273  hmeoimaf1o  23274  haushmphlem  23291  tsmsf1o  23649  imasdsf1olem  23879  imasf1oxmet  23881  imasf1oxms  23998  ovoliunlem1  25019  dyadmbl  25117  vitalilem3  25127  dvcnvlem  25493  dvne0f1  25529  dvcnvrelem2  25535  logf1o2  26158  dvlog  26159  wilthlem3  26574  istrkg2ld  27711  f1otrg  28122  axcontlem10  28231  usgrf1  28432  usgrexmplef  28516  usgrres1  28572  edgusgrnbfin  28630  usgrexilem  28697  sizusglecusglem1  28718  uspgr2wlkeq  28903  trlres  28957  usgr2trlncl  29017  clwlkclwwlk  29255  adjbd1o  31338  padct  31944  s1f1  32109  s2f1  32111  cycpmconjv  32301  lmimdim  32689  madjusmdetlem4  32810  tpr2rico  32892  qqhre  33000  indf1ofs  33024  eulerpartgbij  33371  eulerpartlemgh  33377  ballotlemscr  33517  ballotlemro  33521  ballotlemfrc  33525  ballotlemrinv0  33531  reprpmtf1o  33638  derangenlem  34162  subfacp1lem3  34173  subfacp1lem5  34175  erdsze2lem1  34194  cvmliftmolem1  34272  cvmlift2lem9a  34294  phpreu  36472  poimirlem1  36489  poimirlem4  36492  poimirlem9  36497  poimirlem22  36510  mblfinlem2  36526  metf1o  36623  ismtyima  36671  ismtyres  36676  rngoisocnv  36849  laut11  38957  diaf1oN  40001  mapdcnvcl  40523  mapdcnvid2  40528  ricdrng1  41102  evlselv  41159  eldioph2lem2  41499  eldioph2  41500  pwfi2f1o  41838  gicabl  41841  sge0f1o  45098  nnfoctbdjlem  45171  f1ocof1ob2  45790  f1oresf1o  45998  fundcmpsurbijinjpreimafv  46075  fundcmpsurinjpreimafv  46076  fundcmpsurinjimaid  46079  isomuspgrlem1  46495  isomuspgrlem2c  46498  isomgrsym  46504  xpsrngd  46680