Theorem f1of1 6602

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

Syntax hints:   → wi 4  –1-1→wf1 6333  –onto→wfo 6334  –1-1-onto→wf1o 6335

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 6343

This theorem is referenced by:  f1of  6603  f1sng  6644  f1oresrab  6881  f1prex  7033  f1ocnvfvrneq  7035  isof1oidb  7072  isores3  7083  isoini2  7087  isosolem  7095  f1oiso  7099  weniso  7102  weisoeq  7103  f1opw2  7397  f1ovv  7664  tposf12  7928  oacomf1olem  8201  enssdom  8553  sucdom2  8648  domssex2  8699  mapen  8703  ssenen  8713  phplem4  8721  php3  8725  ssfi  8760  f1finf1o  8767  domunfican  8817  fiint  8821  f1opwfi  8854  mapfienlem1  8895  mapfienlem2  8896  mapfien  8898  marypha1lem  8923  ordtypelem10  9017  oiexg  9025  unxpwdom2  9078  wemapwe  9186  inlresf1  9370  inrresf1  9372  isinffi  9447  infxpenlem  9466  fseqenlem1  9477  dfac12lem2  9597  dfac12r  9599  ackbij2  9696  cff1  9711  infpssrlem4  9759  fin4en1  9762  enfin2i  9774  fin23lem28  9793  isf32lem7  9812  isf34lem3  9828  enfin1ai  9837  canthnum  10102  canthwe  10104  canthp1lem2  10106  pwfseqlem4  10115  pwfseqlem5  10116  tskuni  10236  grothomex  10282  negfi  11619  seqf1olem1  13452  hashfacen  13855  hashfacenOLD  13856  hashf1lem1  13857  hashf1lem1OLD  13858  fsumss  15123  ackbijnn  15224  fprodss  15343  bitsinv2  15835  bitsf1  15838  sadasslem  15862  sadeq  15864  phimullem  16164  eulerthlem2  16167  unbenlem  16292  f1ocpbllem  16848  f1ovscpbl  16850  xpsff1o2  16893  xpsmnd  18010  injsubmefmnd  18121  xpsgrp  18278  eqgen  18393  conjsubgen  18451  subggim  18466  gicsubgen  18478  symgfvne  18569  symgextf1  18609  symgfixelsi  18623  f1omvdmvd  18631  f1omvdconj  18634  pmtrfconj  18654  odngen  18762  sylow1lem2  18784  sylow2blem1  18805  gsumzres  19090  gsumzcl2  19091  gsumzf1o  19093  gsumzaddlem  19102  gsumconst  19115  gsumzmhm  19118  gsumzoppg  19125  dprdf1o  19215  gim0to0  19558  gsumfsum  20226  zntoslem  20317  znunithash  20325  iporthcom  20393  lindfres  20581  islindf3  20584  lindsmm  20586  lmimlbs  20594  lbslcic  20599  coe1sfi  20930  coe1mul2lem2  20985  resthauslem  22056  sshauslem  22065  basqtop  22404  tgqtop  22405  hmeoopn  22459  hmeocld  22460  hmeontr  22462  hmeoimaf1o  22463  haushmphlem  22480  tsmsf1o  22838  imasdsf1olem  23068  imasf1oxmet  23070  imasf1oxms  23184  ovoliunlem1  24195  dyadmbl  24293  vitalilem3  24303  dvcnvlem  24668  dvne0f1  24704  dvcnvrelem2  24710  logf1o2  25333  dvlog  25334  wilthlem3  25747  istrkg2ld  26346  f1otrg  26757  axcontlem10  26859  usgrf1  27057  usgrexmplef  27141  usgrres1  27197  edgusgrnbfin  27255  usgrexilem  27322  sizusglecusglem1  27343  uspgr2wlkeq  27527  trlres  27582  usgr2trlncl  27641  clwlkclwwlk  27879  adjbd1o  29960  padct  30571  s1f1  30734  s2f1  30736  cycpmconjv  30928  madjusmdetlem4  31294  tpr2rico  31376  qqhre  31482  indf1ofs  31506  eulerpartgbij  31851  eulerpartlemgh  31857  ballotlemscr  31997  ballotlemro  32001  ballotlemfrc  32005  ballotlemrinv0  32011  reprpmtf1o  32118  derangenlem  32642  subfacp1lem3  32653  subfacp1lem5  32655  erdsze2lem1  32674  cvmliftmolem1  32752  cvmlift2lem9a  32774  phpreu  35314  poimirlem1  35331  poimirlem4  35334  poimirlem9  35339  poimirlem22  35352  mblfinlem2  35368  metf1o  35466  ismtyima  35514  ismtyres  35519  rngoisocnv  35692  laut11  37655  diaf1oN  38699  mapdcnvcl  39221  mapdcnvid2  39226  eldioph2lem2  40068  eldioph2  40069  pwfi2f1o  40406  gicabl  40409  sge0f1o  43380  nnfoctbdjlem  43453  f1oresf1o  44207  fundcmpsurbijinjpreimafv  44285  fundcmpsurinjpreimafv  44286  fundcmpsurinjimaid  44289  isomuspgrlem1  44705  isomuspgrlem2c  44708  isomgrsym  44714