Theorem f1of1 6699

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

Syntax hints:   → wi 4  –1-1→wf1 6415  –onto→wfo 6416  –1-1-onto→wf1o 6417

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 396  df-f1o 6425

This theorem is referenced by:  f1of  6700  f1sng  6741  f1oresrab  6981  f1prex  7136  f1ocnvfvrneq  7138  isof1oidb  7175  isores3  7186  isoini2  7190  isosolem  7198  f1oiso  7202  weniso  7205  weisoeq  7206  f1opw2  7502  f1ovv  7774  tposf12  8038  oacomf1olem  8357  enssdom  8720  sucdom2  8822  domssex2  8873  mapen  8877  ssenen  8887  phplem4  8895  php3  8899  ssfiALT  8919  ssdomfi  8940  f1finf1o  8975  domunfican  9017  fiint  9021  f1opwfi  9053  mapfienlem1  9094  mapfienlem2  9095  mapfien  9097  marypha1lem  9122  ordtypelem10  9216  oiexg  9224  unxpwdom2  9277  wemapwe  9385  inlresf1  9604  inrresf1  9606  isinffi  9681  infxpenlem  9700  fseqenlem1  9711  dfac12lem2  9831  dfac12r  9833  ackbij2  9930  cff1  9945  infpssrlem4  9993  fin4en1  9996  enfin2i  10008  fin23lem28  10027  isf32lem7  10046  isf34lem3  10062  enfin1ai  10071  canthnum  10336  canthwe  10338  canthp1lem2  10340  pwfseqlem4  10349  pwfseqlem5  10350  tskuni  10470  grothomex  10516  negfi  11854  seqf1olem1  13690  hashfacen  14094  hashfacenOLD  14095  hashf1lem1  14096  hashf1lem1OLD  14097  fsumss  15365  ackbijnn  15468  fprodss  15586  bitsinv2  16078  bitsf1  16081  sadasslem  16105  sadeq  16107  phimullem  16408  eulerthlem2  16411  unbenlem  16537  f1ocpbllem  17152  f1ovscpbl  17154  xpsff1o2  17197  xpsmnd  18340  injsubmefmnd  18451  xpsgrp  18609  eqgen  18724  conjsubgen  18782  subggim  18797  gicsubgen  18809  symgfvne  18903  symgextf1  18944  symgfixelsi  18958  f1omvdmvd  18966  f1omvdconj  18969  pmtrfconj  18989  odngen  19097  sylow1lem2  19119  sylow2blem1  19140  gsumzres  19425  gsumzcl2  19426  gsumzf1o  19428  gsumzaddlem  19437  gsumconst  19450  gsumzmhm  19453  gsumzoppg  19460  dprdf1o  19550  gim0to0  19901  gsumfsum  20577  zntoslem  20676  znunithash  20684  iporthcom  20752  lindfres  20940  islindf3  20943  lindsmm  20945  lmimlbs  20953  lbslcic  20958  coe1sfi  21294  coe1mul2lem2  21349  resthauslem  22422  sshauslem  22431  basqtop  22770  tgqtop  22771  hmeoopn  22825  hmeocld  22826  hmeontr  22828  hmeoimaf1o  22829  haushmphlem  22846  tsmsf1o  23204  imasdsf1olem  23434  imasf1oxmet  23436  imasf1oxms  23551  ovoliunlem1  24571  dyadmbl  24669  vitalilem3  24679  dvcnvlem  25045  dvne0f1  25081  dvcnvrelem2  25087  logf1o2  25710  dvlog  25711  wilthlem3  26124  istrkg2ld  26725  f1otrg  27136  axcontlem10  27244  usgrf1  27445  usgrexmplef  27529  usgrres1  27585  edgusgrnbfin  27643  usgrexilem  27710  sizusglecusglem1  27731  uspgr2wlkeq  27915  trlres  27970  usgr2trlncl  28029  clwlkclwwlk  28267  adjbd1o  30348  padct  30956  s1f1  31119  s2f1  31121  cycpmconjv  31311  madjusmdetlem4  31682  tpr2rico  31764  qqhre  31870  indf1ofs  31894  eulerpartgbij  32239  eulerpartlemgh  32245  ballotlemscr  32385  ballotlemro  32389  ballotlemfrc  32393  ballotlemrinv0  32399  reprpmtf1o  32506  derangenlem  33033  subfacp1lem3  33044  subfacp1lem5  33046  erdsze2lem1  33065  cvmliftmolem1  33143  cvmlift2lem9a  33165  phpreu  35688  poimirlem1  35705  poimirlem4  35708  poimirlem9  35713  poimirlem22  35726  mblfinlem2  35742  metf1o  35840  ismtyima  35888  ismtyres  35893  rngoisocnv  36066  laut11  38027  diaf1oN  39071  mapdcnvcl  39593  mapdcnvid2  39598  eldioph2lem2  40499  eldioph2  40500  pwfi2f1o  40837  gicabl  40840  sge0f1o  43810  nnfoctbdjlem  43883  f1ocof1ob2  44461  f1oresf1o  44669  fundcmpsurbijinjpreimafv  44747  fundcmpsurinjpreimafv  44748  fundcmpsurinjimaid  44751  isomuspgrlem1  45167  isomuspgrlem2c  45170  isomgrsym  45176