Theorem f1of1 6589

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

Syntax hints:   → wi 4  –1-1→wf1 6321  –onto→wfo 6322  –1-1-onto→wf1o 6323

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 400  df-f1o 6331

This theorem is referenced by:  f1of  6590  f1sng  6631  f1oresrab  6866  f1prex  7018  f1ocnvfvrneq  7020  isof1oidb  7056  isores3  7067  isoini2  7071  isosolem  7079  f1oiso  7083  weniso  7086  weisoeq  7087  f1opw2  7380  f1ovv  7641  tposf12  7900  oacomf1olem  8173  enssdom  8517  sucdom2  8610  domssex2  8661  mapen  8665  ssenen  8675  phplem4  8683  php3  8687  ssfi  8722  f1finf1o  8729  domunfican  8775  fiint  8779  f1opwfi  8812  mapfienlem1  8852  mapfienlem2  8853  mapfien  8855  marypha1lem  8881  ordtypelem10  8975  oiexg  8983  unxpwdom2  9036  wemapwe  9144  inlresf1  9328  inrresf1  9330  isinffi  9405  infxpenlem  9424  fseqenlem1  9435  dfac12lem2  9555  dfac12r  9557  ackbij2  9654  cff1  9669  infpssrlem4  9717  fin4en1  9720  enfin2i  9732  fin23lem28  9751  isf32lem7  9770  isf34lem3  9786  enfin1ai  9795  canthnum  10060  canthwe  10062  canthp1lem2  10064  pwfseqlem4  10073  pwfseqlem5  10074  tskuni  10194  grothomex  10240  negfi  11577  seqf1olem1  13405  hashfacen  13808  hashf1lem1  13809  fsumss  15074  ackbijnn  15175  fprodss  15294  bitsinv2  15782  bitsf1  15785  sadasslem  15809  sadeq  15811  phimullem  16106  eulerthlem2  16109  unbenlem  16234  f1ocpbllem  16789  f1ovscpbl  16791  xpsff1o2  16834  xpsmnd  17943  injsubmefmnd  18054  xpsgrp  18210  eqgen  18325  conjsubgen  18383  subggim  18398  gicsubgen  18410  symgfvne  18501  symgextf1  18541  symgfixelsi  18555  f1omvdmvd  18563  f1omvdconj  18566  pmtrfconj  18586  odngen  18694  sylow1lem2  18716  sylow2blem1  18737  gsumzres  19022  gsumzcl2  19023  gsumzf1o  19025  gsumzaddlem  19034  gsumconst  19047  gsumzmhm  19050  gsumzoppg  19057  dprdf1o  19147  gim0to0  19490  gsumfsum  20158  zntoslem  20248  znunithash  20256  iporthcom  20324  lindfres  20512  islindf3  20515  lindsmm  20517  lmimlbs  20525  lbslcic  20530  coe1sfi  20842  coe1mul2lem2  20897  resthauslem  21968  sshauslem  21977  basqtop  22316  tgqtop  22317  hmeoopn  22371  hmeocld  22372  hmeontr  22374  hmeoimaf1o  22375  haushmphlem  22392  tsmsf1o  22750  imasdsf1olem  22980  imasf1oxmet  22982  imasf1oxms  23096  ovoliunlem1  24106  dyadmbl  24204  vitalilem3  24214  dvcnvlem  24579  dvne0f1  24615  dvcnvrelem2  24621  logf1o2  25241  dvlog  25242  wilthlem3  25655  istrkg2ld  26254  f1otrg  26665  axcontlem10  26767  usgrf1  26965  usgrexmplef  27049  usgrres1  27105  edgusgrnbfin  27163  usgrexilem  27230  sizusglecusglem1  27251  uspgr2wlkeq  27435  trlres  27490  usgr2trlncl  27549  clwlkclwwlk  27787  adjbd1o  29868  padct  30481  s1f1  30645  s2f1  30647  cycpmconjv  30834  madjusmdetlem4  31183  tpr2rico  31265  qqhre  31371  indf1ofs  31395  eulerpartgbij  31740  eulerpartlemgh  31746  ballotlemscr  31886  ballotlemro  31890  ballotlemfrc  31894  ballotlemrinv0  31900  reprpmtf1o  32007  derangenlem  32531  subfacp1lem3  32542  subfacp1lem5  32544  erdsze2lem1  32563  cvmliftmolem1  32641  cvmlift2lem9a  32663  phpreu  35041  poimirlem1  35058  poimirlem4  35061  poimirlem9  35066  poimirlem22  35079  mblfinlem2  35095  metf1o  35193  ismtyima  35241  ismtyres  35246  rngoisocnv  35419  laut11  37382  diaf1oN  38426  mapdcnvcl  38948  mapdcnvid2  38953  eldioph2lem2  39702  eldioph2  39703  pwfi2f1o  40040  gicabl  40043  sge0f1o  43021  nnfoctbdjlem  43094  f1oresf1o  43846  fundcmpsurbijinjpreimafv  43924  fundcmpsurinjpreimafv  43925  fundcmpsurinjimaid  43928  isomuspgrlem1  44345  isomuspgrlem2c  44348  isomgrsym  44354